Documentation

Lean 4 Proof

theorem weighted_oscillation_spectrum
    (N : ℕ) (e : WeightedNSectorEconomy N) :
    -- Oscillation periods depend on weight configuration through eigenvalue spectrum
    -- Equal weights: single period T = 2π/ω
    -- General weights: spectrum of periods T_k = 2π/ω_k
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:463

Module Section

## Proposition 3b.5: Oscillation Spectrum with Weights

In the same file