Eps PQ

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def epsPQ (e : TwoWorldEconomy N) (n : Fin N) : ℝ :=
  e.ℓ n / e.v_price n

Dependency Graph

Used by

indicator_classification_foundations composed_ordering epsPQ_lt_one epsPQ_pos temporal_rules_summary

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:56

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file

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