Documentation

Lean 4 Proof

theorem minsky_friction_spiral {β_L V T β_C K_eff Tstar β_I G T_min β_S E ξ : ℝ}
    (h : -(learningFrictionRate β_L V T + institutionalFrictionRate β_I G T T_min
           + shockFrictionImpulse β_S E ξ)
         < cascadeFrictionRate β_C K_eff T Tstar) :
    0 < combinedFrictionRate β_L V T β_C K_eff Tstar β_I G T_min β_S E ξ := by
  simp only [combinedFrictionRate]
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:134

Module Section

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

In the same file