Documentation

Lean 4 Proof

theorem marketClearing_full_speed {v_price : ℝ} :
    administeredSpeed v_price 0 = v_price := by
  simp [administeredSpeed]

Dependency Graph

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:167

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file