Documentation

Lean 4 Proof

private theorem variance_identity
    (P : Fin J → ℝ) (f : Fin J → ℝ)
    (hsum : ∑ j : Fin J, P j = 1) :
    (∑ j, P j * f j ^ 2) - (∑ j, P j * f j) ^ 2 =
    ∑ j, P j * (f j - ∑ k, P k * f k) ^ 2 := by
  set μ := ∑ k, P k * f k
  have expand : ∀ j : Fin J,
      P j * (f j - μ) ^ 2 = P j * f j ^ 2 - 2 * μ * (P j * f j) + μ ^ 2 * P j := by
    intro j; ring
  simp_rw [expand]
  rw [Finset.sum_add_distrib, Finset.sum_sub_distrib]
  simp_rw [← Finset.mul_sum]
  rw [hsum]; ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CESEstimation.lean:443

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file