Documentation

Lean 4 Proof

theorem weighted_vri
    (N : ℕ) (e : WeightedNSectorEconomy N) (n : Fin N) :
    -- Σ_kk = T / |μ_k| in eigenmode basis
    -- Higher variance for smaller |μ_k| (slower modes more volatile)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:261

Module Section

## Theorem 3b.2: Weighted VRI (merged from WeightedVRI.lean)

In the same file