Documentation

Lean 4 Proof

theorem two_world_inherits_paper3 (e : TwoWorldEconomy N) (n : Fin N)
    (hKeff : 0 < sectorEffectiveCurvature e.toNSectorEconomy n) :
    0 < sectorRelaxRate e.toNSectorEconomy n :=
  landscape_structure e.toNSectorEconomy n hKeff

Dependency Graph

Location

thesis/CESProofs/Dynamics/TwoWorldDefs.lean:164

Module Section

Two-World Economy: Price vs. Production Timescale Separation

In the same file