isw_driver

formal source

  20-/
  21
  22/-- The ISW driver B(a,k) = -1 + f + dlnw/dlna. -/
  23noncomputable def isw_driver (P : KernelParams) (k a : ℝ) : ℝ :=
  24  let f := f_growth_eds_ilg P k a
  25  let Xinv := a / (k * P.tau0)
  26  let dlnw := (P.alpha * P.C * Xinv ^ P.alpha) / (1 + P.C * Xinv ^ P.alpha)
  27  -1 + f + dlnw
  28
  29/-- Lemma: In ILG baseline, the growth rate f is greater than 1. -/
  30theorem f_growth_gt_one (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k)
  31    (halpha : 0 < P.alpha) (hC : 0 < P.C) :
  32    1 < f_growth_eds_ilg P k a := by
  33  set Xinv := a / (k * P.tau0)
  34  set B := growth_prefactor P.alpha P.C
  35  have hB : 0 < B := by
  36    unfold growth_prefactor
  37    apply div_pos
  38    · linarith
  39    · nlinarith
  40  have hXinv : 0 < Xinv := div_pos ha (mul_pos hk P.tau0_pos)
  41  have hXinv_pow : 0 < Xinv ^ P.alpha := rpow_pos_of_pos hXinv _
  42  unfold f_growth_eds_ilg
  43  -- f = (1 + B(1+alpha)X^alpha) / (1 + BX^alpha)
  44  -- 1 < (1 + BX^alpha + B*alpha*X^alpha) / (1 + BX^alpha)
  45  -- 1 < 1 + (B*alpha*X^alpha) / (1 + BX^alpha)
  46  field_simp
  47  apply lt_add_of_pos_right
  48  apply div_pos
  49  · repeat apply mul_pos <;> assumption
  50  · apply add_pos_of_pos_of_nonneg
  51    · exact one_pos
  52    · repeat apply mul_nonneg <;> (try exact le_of_lt hB) <;> (try exact le_of_lt hXinv_pow)
  53