theorem
proved
tactic proof
D_growth_ge_a
show as:
view Lean formalization →
formal statement (Lean)
79theorem D_growth_ge_a (a k tau0 : ℝ) (ha : 0 < a) (hk : 0 < k) (ht : 0 < tau0) :
80 a ≤ D_growth a k tau0 := by
proof body
Tactic-mode proof.
81 unfold D_growth
82 have hbeta := beta_growth_pos k tau0 hk ht
83 have ha_pow : 0 < a ^ alphaLock := Real.rpow_pos_of_pos ha _
84 have h_inner : 1 ≤ 1 + beta_growth k tau0 * a ^ alphaLock := by
85 linarith [mul_pos hbeta ha_pow]
86 have h_exp : 0 < 1 / (1 + alphaLock) := by
87 apply div_pos one_pos
88 linarith [alphaLock_pos]
89 calc a = a * 1 := by ring
90 _ ≤ a * (1 + beta_growth k tau0 * a ^ alphaLock) ^ (1 / (1 + alphaLock)) := by
91 apply mul_le_mul_of_nonneg_left _ (le_of_lt ha)
92 exact Real.one_le_rpow h_inner h_exp.le
93
94/-! ## The Growth Rate f(a,k) -/
95
96/-- The ILG-modified growth rate.
97 f(a,k) = d ln D / d ln a
98 = 1 + [α/(1+α)] * β*a^α / (1 + β*a^α)
99
100 In GR (β = 0): f = 1 (matter domination).
101 Under ILG: f > 1 (enhanced growth rate). -/