Documentation

Lean 4 Proof

theorem convergenceRate_nonneg (J : ℕ) (ρ c T Tstar : ℝ) :
    0 ≤ convergenceRate J ρ c T Tstar := by
  simp only [convergenceRate]
  exact mul_nonneg (abs_nonneg _) (le_max_left 0 _)

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:198

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file