Documentation

Lean 4 Proof

theorem algebraic_vri_core (P x : Fin J → ℝ)
    (_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 := by
  simp only
  set μ := ∑ j, x j * P j
  have expand : ∀ j, P j * x j * (x j - μ) = x j ^ 2 * P j - μ * (x j * P j) := by
    intro j; ring
  simp_rw [expand, Finset.sum_sub_distrib, ← Finset.mul_sum]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:131

Module Section

### The Variance-Response Identity

In the same file