Documentation

Lean 4 Proof

theorem oscillation_spectrum (e : NSectorEconomy N) :
    -- Eigenvalues of (J-R)*H have complex conjugate pairs
    -- with negative real parts (stable oscillations)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:80

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file