Documentation

Lean 4 Proof

theorem variance_centered_form (P x : Fin J → ℝ)
    (hP_sum : ∑ j, P j = 1) :
    let μ := ∑ j, x j * P j
    (∑ j, x j ^ 2 * P j) - μ ^ 2 =
    ∑ j, P j * (x j - μ) ^ 2 := by
  simp only
  set μ := ∑ j, x j * P j
  have expand : ∀ j, P j * (x j - μ) ^ 2 =
    x j ^ 2 * P j - 2 * μ * (x j * P j) + μ ^ 2 * P j := by
    intro j; ring
  simp_rw [expand, Finset.sum_add_distrib, Finset.sum_sub_distrib,
    ← Finset.mul_sum, hP_sum]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:145

Module Section

### The Variance-Response Identity

In the same file