Documentation

Lean 4 Proof

theorem learning_reduces_friction {β_L V T : ℝ}
    (hβ : 0 < β_L) (hV : 0 < V) (hT : 0 < T) :
    learningFrictionRate β_L V T < 0 := by
  simp only [learningFrictionRate]
  linarith [mul_pos hβ (mul_pos hV hT)]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:68

Module Section

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

In the same file