Documentation

Lean 4 Proof

theorem learning_at_zero {β_L V : ℝ} :
    learningFrictionRate β_L V 0 = 0 := by
  simp only [learningFrictionRate, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousT.lean:186

Module Section

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

In the same file