Documentation

Lean 4 Proof

theorem variance_nonneg (P x : Fin J → ℝ)
    (hP_sum : ∑ j, P j = 1)
    (hP_pos : ∀ j, 0 ≤ P j) :
    0 ≤ (∑ j, x j ^ 2 * P j) - (∑ j, x j * P j) ^ 2 := by
  rw [variance_centered_form P x hP_sum]
  exact Finset.sum_nonneg fun j _ => mul_nonneg (hP_pos j) (sq_nonneg _)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:160

Module Section

### The Variance-Response Identity

In the same file