Documentation

Lean 4 Proof

theorem cascade_increases_friction {β_C K_eff T Tstar : ℝ}
    (hβ : 0 < β_C) (hK : 0 < K_eff) (hT : T < Tstar) :
    0 < cascadeFrictionRate β_C K_eff T Tstar := by
  simp only [cascadeFrictionRate]
  exact mul_pos (mul_pos hβ hK) (by linarith)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:84

Module Section

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

In the same file