Documentation

Lean 4 Proof

theorem institutional_reform_lowers_friction {β_I G T T_min : ℝ}
    (hβ : 0 < β_I) (hG : 0 < G) (hT : T_min < T) :
    institutionalFrictionRate β_I G T T_min < 0 := by
  simp only [institutionalFrictionRate]
  linarith [mul_pos hβ (mul_pos hG (by linarith : 0 < T - T_min))]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:99

Module Section

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

In the same file