Documentation

Lean 4 Proof

theorem critical_damping {ω : ℝ} (hω : 0 < ω) :
    dampingRatio ω ω = 1 := by
  simp only [dampingRatio]
  exact div_self (ne_of_gt hω)

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:254

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file