Documentation

Lean 4 Proof

theorem endogenous_cycle_existence (e : NSectorEconomy N)
    (hN : 2 ≤ N) :
    -- There exists a stable limit cycle when the antisymmetric
    -- coupling is non-zero and the system is underdamped
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/PhillipsCycles.lean:93

Module Section

Results 63-69: Phillips Curve, Endogenous Cycles, and Oscillation Energy

In the same file