No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
268noncomputable def shiftedOfH (x : ℝ) (hx : 0 < x) : ShiftedCarrier :=
proof body
Definition body.
269 ⟨H x, by
270 have hHx : 1 ≤ H x := H_ge_one x hx
271 linarith⟩
272
273/-- The narrower `[1, ∞)` range supporting the actual values of `H`. -/
depends on (9)
Lean names referenced from this declaration's body.
-
H
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
H_ge_one
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
ShiftedCarrier
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
H
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use