Documentation

Lean 4 Proof

theorem oscillation_energy_decay {M : ℕ}
    (R : Fin M -> Fin M -> ℝ) (hR : IsPosSemidef R)
    (Hxi : Fin M -> ℝ) :
    0 ≤ ∑ i, ∑ j, R i j * Hxi i * Hxi j :=
  hR Hxi

Dependency Graph

Location

thesis/CESProofs/Dynamics/PhillipsCycles.lean:136

Module Section

Results 63-69: Phillips Curve, Endogenous Cycles, and Oscillation Energy

In the same file