Timescale Gap

Documentation

Lean 4 Proof

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

Dependency Graph

Used by

crisis_asymmetry_ratio timescaleGap_gt_one

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:176

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file

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