Documentation

Lean 4 Proof

theorem timescaleGap_gt_one (e : TwoWorldEconomy N) (n : Fin N)
    (hr : 0 < sectorRelaxRate e.toNSectorEconomy n)
    (hbound : sectorRelaxRate e.toNSectorEconomy n < e.v_price n) :
    1 < timescaleGap e n hr := by
  simp only [timescaleGap]
  exact Bound.one_lt_div_of_pos_of_lt hr hbound

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:181

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file