Documentation

Lean 4 Proof

theorem convergenceRate_pos (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c)
    {T Tstar : ℝ} (hTs : 0 < Tstar) (hTlt : T < Tstar) :
    0 < convergenceRate J ρ c T Tstar := by
  simp only [convergenceRate]
  apply mul_pos
  · rw [abs_pos]
    exact ne_of_lt (logCesEigenvaluePerp_neg hρ (by omega) hc)
  · rw [lt_max_iff]; right
    rw [sub_pos, div_lt_one hTs]
    exact hTlt

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:204

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file