Documentation

Lean 4 Proof

theorem epsPQ_pos (e : TwoWorldEconomy N) (n : Fin N) :
    0 < epsPQ e n := by
  simp only [epsPQ]
  exact div_pos (e.hℓ n) (e.hv n)

Dependency Graph

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:60

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file