growth_prefactor

formal source

   9
  10/-- The prefactor for the first-order ILG growth correction in EdS background.
  11    Derived from plugging D = a(1 + B a^alpha) into the growth ODE. -/
  12noncomputable def growth_prefactor (alpha C : ℝ) : ℝ :=
  13  (3 * C) / (2 * alpha^2 + 5 * alpha)
  14
  15/-- The closed-form ILG growth factor D(a, k) in EdS background (first-order in C). -/
  16noncomputable def growth_eds_ilg (P : KernelParams) (k a : ℝ) : ℝ :=
  17  a * (1 + (growth_prefactor P.alpha P.C) * (a / (k * P.tau0)) ^ P.alpha)
  18
  19/-- Growth rate f = d ln D / d ln a for the ILG growth factor. -/
  20noncomputable def f_growth_eds_ilg (P : KernelParams) (k a : ℝ) : ℝ :=
  21  let Xinv := a / (k * P.tau0)
  22  let B := growth_prefactor P.alpha P.C
  23  (1 + B * (1 + P.alpha) * Xinv ^ P.alpha) / (1 + B * Xinv ^ P.alpha)
  24
  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