Price Relax Time

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def priceRelaxTime (e : TwoWorldEconomy N) (n : Fin N) : ℝ :=
  1 / e.v_price n

Dependency Graph

Used by

priceRelaxTime_pos price_leads_quantity price_faster_than_quantity

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:78

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file

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