Documentation

Lean 4 Proof

theorem slow_fast_asymmetry (epsilon : ℝ) (h_eps : 0 < epsilon) (h_small : epsilon < 1) :
    -- Expansion timescale exceeds contraction timescale by factor 1/ε > 1
    1 < 1 / epsilon := by
  rw [one_div, one_lt_inv_iff₀]
  exact ⟨h_eps, h_small⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:241

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file