Documentation

Lean 4 Proof

theorem priceRelaxTime_pos (e : TwoWorldEconomy N) (n : Fin N) :
    0 < priceRelaxTime e n := by
  simp only [priceRelaxTime]
  exact div_pos one_pos (e.hv n)

Dependency Graph

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:93

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file