def
definition
def or abbrev
GrowthODE_ILG
show as:
view Lean formalization →
formal statement (Lean)
28def GrowthODE_ILG (P : KernelParams) (k : ℝ) (D_func : ℝ → ℝ) : Prop :=
proof body
Definition body.
29 ∀ a, 0 < a →
30 let w := kernel P k a
31 -- Expressed in terms of derivatives w.r.t a:
32 -- a² D'' + (3/2) a D' - (3/2) w D = 0
33 a^2 * (deriv (deriv D_func) a) + (3/2 : ℝ) * a * (deriv D_func a) - (3/2 : ℝ) * w * D_func a = 0
34
35/-- Theorem: The closed-form growth factor satisfies the ILG-modified growth ODE
36 to first order in C (neglecting O(C²) terms). -/