Documentation

Lean 4 Proof

theorem multi_modal_relaxation_spectrum
    (J N : ℕ) (e : WeightedNSectorEconomy N) (n : Fin N) :
    -- At general weights: J-1 distinct eigenvalues from secular equation
    -- Observable: impulse responses are sums of exponentials, not single exponential
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:379

Module Section

## Theorem 3b.1: General-Weight Relaxation Spectrum

In the same file