Quantity Relax Time

Documentation

Lean 4 Proof

def quantityRelaxTime (e : TwoWorldEconomy N) (n : Fin N)
    (_hr : 0 < sectorRelaxRate e.toNSectorEconomy n) : ℝ :=
  1 / sectorRelaxRate e.toNSectorEconomy n

Dependency Graph

Used by

quantityRelaxTime_pos price_leads_quantity price_faster_than_quantity curvature_conservation_lag

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:88

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file

TwoWorldEconomy epsPQ epsPQ_pos epsPQ_lt_one priceRelaxTime priceRelaxTime_pos quantityRelaxTime_pos price_faster_than_quantity slow_manifold_reduction two_world_inherits_paper3 timescaleGap timescaleGap_gt_one timescaleGap_monotone_in_relaxRate