← Mathematical handbook

Equality in the finite quadratic mean inequality

theorem Verification.finite_centered_square_sum (n : ℕ) (hn : 0 < n) (d : Fin n → ℝ) : ∑ i : Fin n, (d i - (∑ j : Fin n, d j) / ↑n) ^ 2 = ∑ i : Fin n, d i ^ 2 - (∑ i : Fin n, d i) ^ 2 / ↑n

theorem Verification.finite_cauchy_equality_iff (n : ℕ) (hn : 0 < n) (d : Fin n → ℝ) : ∑ i : Fin n, d i ^ 2 = (∑ i : Fin n, d i) ^ 2 / ↑n ↔ ∀ (i : Fin n), d i = (∑ j : Fin n, d j) / ↑n