GrowthODE_ILG

formal source

  25/-- The ILG-modified growth ODE in EdS background (Target B).
  26    Using ln(a) as the independent variable:
  27    D'' + (1/2) D' - (3/2) w(a,k) D = 0 -/
  28def GrowthODE_ILG (P : KernelParams) (k : ℝ) (D_func : ℝ → ℝ) : Prop :=
  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). -/
  37theorem growth_satisfies_ode (P : KernelParams) (k : ℝ) (hk : 0 < k) :
  38    let B := growth_prefactor P.alpha P.C
  39    let D := fun a => a * (1 + B * (a / (k * P.tau0)) ^ P.alpha)
  40    ∀ a, 0 < a →
  41      (0.01 : ℝ) ≤ (a / (k * P.tau0)) →
  42      let w := kernel P k a
  43      let Xinv := (a / (k * P.tau0))
  44      let error_term := (3/2 : ℝ) * P.C * B * Xinv ^ (2 * P.alpha) * a
  45      a^2 * (deriv (deriv D) a) + (3/2 : ℝ) * a * (deriv D a) - (3/2 : ℝ) * w * D a + error_term = 0 := by
  46  intro B D a ha hXinv_large
  47  unfold growth_prefactor kernel
  48  set C := P.C
  49  set α := P.alpha
  50  set τ₀ := P.tau0
  51  set Xinv := a / (k * τ₀)
  52  -- D(a) = a + B * (k*τ₀)^(-α) * a^(1+α)
  53  have hD : D = fun a => a + B * (k * τ₀) ^ (-α) * a ^ (1 + α) := by
  54    funext a'; simp [D]
  55    rw [div_rpow (le_of_lt ha) (mul_nonneg (le_of_lt hk) (le_of_lt P.tau0_pos))]
  56    rw [Real.rpow_neg (mul_pos hk P.tau0_pos)]
  57    ring
  58  -- Compute derivatives