Documentation

Lean 4 Proof

theorem sector_vri (e : NSectorEconomy N) (n : Fin N)
    (P : Fin (e.J n) → ℝ) (x : Fin (e.J n) → ℝ)
    (hP_sum : ∑ j, P j = 1) :
    let μ := ∑ j, x j * P j
    ∑ j, P j * x j * (x j - μ) = (∑ j, x j ^ 2 * P j) - μ ^ 2 :=
  algebraic_vri_core P x hP_sum

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:66

Module Section

Results 8-16: Variance-Response Identity and Early Warning

In the same file