Documentation

Lean 4 Proof

theorem weighted_variance_nonneg
    (P w : Fin J → ℝ)
    (hP_nonneg : ∀ j, 0 ≤ P j)
    (hP_sum : ∑ j, P j = 1) :
    0 ≤ (∑ k, P k * w k ^ 2) -
      (∑ k, P k * w k) ^ 2 := by
  set μ := ∑ k, P k * w k
  suffices h : 0 ≤ ∑ k, P k * (w k - μ) ^ 2 by
    have expand : (∑ k, P k * (w k - μ) ^ 2) =
        (∑ k, P k * w k ^ 2) - μ ^ 2 := by
      have h1 : ∀ k : Fin J,
          P k * (w k - μ) ^ 2 =
          P k * w k ^ 2 - 2 * μ * (P k * w k) +
          μ ^ 2 * P k := by intro k; ring
      simp_rw [h1]
      simp only [Finset.sum_add_distrib,
        Finset.sum_sub_distrib, ← Finset.mul_sum,
        hP_sum]
      ring
    linarith
  exact Finset.sum_nonneg fun k _ =>
    mul_nonneg (hP_nonneg k) (sq_nonneg _)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:178

Module Section

General CES Hessian at Arbitrary Allocation

In the same file