Documentation

Lean 4 Proof

theorem combined_rate_steady_state {β_L V T β_C K_eff Tstar β_I G T_min β_S E : ℝ}
    (h_balance : learningFrictionRate β_L V T + cascadeFrictionRate β_C K_eff T Tstar
                 + institutionalFrictionRate β_I G T T_min = 0) :
    combinedFrictionRate β_L V T β_C K_eff Tstar β_I G T_min β_S E 0 = 0 := by
  simp only [combinedFrictionRate, shockFrictionImpulse, mul_zero, add_zero]
  exact h_balance

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:199

Module Section

Results T-80 through T-89: Endogenous Information Friction Dynamics

In the same file