Sections / Section 9: CES Potential and Information Friction / convergenceRate

Convergence Rate

defprovedCES Potential

Documentation

Lean 4 Proof

def convergenceRate (J : ℕ) (ρ c T Tstar : ℝ) : ℝ :=
  |logCesEigenvaluePerp J ρ c| * max 0 (1 - T / Tstar)

Dependency Graph

Used by

convergenceRate_pos convergenceRate_nonneg convergenceRate_at_critical

Location

thesis/CESProofs/Potential/Welfare.lean:194

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_nonneg convergenceRate_pos convergenceRate_at_critical K_increases_with_complementarity