Documentation

Lean 4 Proof

theorem friction_channels_oppose {β_L V T β_C K_eff Tstar β_I G T_min : ℝ}
    (hβL : 0 < β_L) (hV : 0 < V) (hT : 0 < T)
    (hβC : 0 < β_C) (hK : 0 < K_eff) (hTlt : T < Tstar)
    (hβI : 0 < β_I) (hG : 0 < G) (hTmin : T_min < T) :
    learningFrictionRate β_L V T < 0
    ∧ 0 < cascadeFrictionRate β_C K_eff T Tstar
    ∧ institutionalFrictionRate β_I G T T_min < 0 :=
  ⟨learning_reduces_friction hβL hV hT,
   cascade_increases_friction hβC hK hTlt,
   institutional_reform_lowers_friction hβI hG hTmin⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:114

Module Section

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

In the same file