theorem proved term proof

`D_growth_gr_limit`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  74theorem D_growth_gr_limit (a : ℝ) (ha : 0 < a) :
  75    a * (1 + 0 * a ^ alphaLock) ^ (1 / (1 + alphaLock)) = a := by

Term-mode proof.

  76  simp [zero_mul, Real.one_rpow]
  77
  78/-- D ≥ a always (ILG enhances or preserves growth). -/

Lean names referenced from this declaration's body.