Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:32

Module Section

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

In the same file