Documentation

Lean 4 Proof

theorem underdamped_iff {r ω : ℝ} (hω : 0 < ω) :
    dampingRatio r ω < 1 ↔ r < ω := by
  simp only [dampingRatio]
  exact div_lt_one hω

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:248

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file