Documentation

Lean 4 Proof

theorem rhoT_limit_cycle :
    -- If the (rho, T) fixed point is unstable and the domain is bounded,
    -- there exists a stable limit cycle (Poincare-Bendixson theorem)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:178

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file