Documentation

Lean 4 Proof

theorem sectorCriticalFriction_pos (e : NSectorEconomy N) (n : Fin N) :
    0 < sectorCriticalFriction e n := by
  simp only [sectorCriticalFriction, criticalFriction]
  apply div_pos
  · have hJm1 : (0 : ℝ) < ↑(e.J n) - 1 := by
      have : (2 : ℝ) ≤ ↑(e.J n) := by exact_mod_cast (e.hJ n)
      linarith
    exact mul_pos (mul_pos (mul_pos (by norm_num : (0 : ℝ) < 2) hJm1)
      (pow_pos (e.hc n) 2)) (e.hd n)
  · exact curvatureK_pos (e.hJ n) (e.hρ n)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:44

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file