Eps PQ Lt One

theorem proved Dynamics & Crises

Documentation

Lean 4 Proof

theorem epsPQ_lt_one (e : TwoWorldEconomy N) (n : Fin N) :
    epsPQ e n < 1 := by
  simp only [epsPQ]
  exact (div_lt_one (e.hv n)).mpr (e.hfast n)

Dependency Graph

Used by

indicator_classification_foundations composed_ordering temporal_rules_summary

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:66

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file

TwoWorldEconomy epsPQ epsPQ_pos 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