Convergence Rate At Critical

theorem proved CES Potential

Documentation

Lean 4 Proof

theorem convergenceRate_at_critical (J : ℕ) (ρ c Tstar : ℝ) (hTs : 0 < Tstar) :
    convergenceRate J ρ c Tstar Tstar = 0 := by
  simp [convergenceRate, div_self (ne_of_gt hTs)]

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:217

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file

simplex_component_le_one tsallis_nonneg management_return_sign productivity_dispersion_amplification dispersion_increases_with_K dmp_search_duration_pos dmp_search_ces dmp_search_complementarity_monotone dmp_friction_lowers_reservation LyapunovProperty dmp_standard_limit convergenceRate convergenceRate_nonneg convergenceRate_pos K_increases_with_complementarity