Documentation

Lean 4 Proof

theorem curvature_conservation_lag (e : TwoWorldEconomy N) (n : Fin N)
    (hr : 0 < sectorRelaxRate e.toNSectorEconomy n) :
    -- The lag is bounded by the quantity relaxation time
    0 < quantityRelaxTime e n hr :=
  quantityRelaxTime_pos e n hr

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:181

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file