Lean 4 Proof

theorem quantitative_asymmetry {epsilon : ℝ} (h_eps : 0 < epsilon) :
    1 < asymmetryRatioCycles epsilon ↔ epsilon < 1 := by
  simp only [asymmetryRatioCycles]
  constructor
  · intro h
    rw [one_div, one_lt_inv_iff₀] at h
    exact h.2
  · intro h
    rw [one_div, one_lt_inv_iff₀]
    exact ⟨h_eps, h⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:264

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file