Documentation

Lean 4 Proof

theorem quantityRelaxTime_pos (e : TwoWorldEconomy N) (n : Fin N)
    (hr : 0 < sectorRelaxRate e.toNSectorEconomy n) :
    0 < quantityRelaxTime e n hr := by
  simp only [quantityRelaxTime]
  exact div_pos one_pos hr

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:99

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file