A sharp variance bound for distinct natural numbers

The main result of this file minimizes the unnormalized empirical variance of a finite set of natural numbers. The proof enumerates the set increasingly, compares all pairwise differences with those of an initial interval, and evaluates the resulting quadratic sum.

theorem LeanPool.ErdosMoser.sumSquaresRange (m : ℕ) : 6 * ∑ i ∈ Finset.range m, ↑i ^ 2 = ↑m * (↑m - 1) * (2 * ↑m - 1)

Closed form for the sum of squares over Finset.range m, stated over the reals for use in the variance calculation.

theorem LeanPool.ErdosMoser.twoMulCardSumSquaresSubSquareEqSumPairsDiffSquare {ι : Type u_1} (s : Finset ι) (g : ι → ℝ) : 2 * (↑s.card * ∑ i ∈ s, g i ^ 2 - (∑ i ∈ s, g i) ^ 2) = ∑ i ∈ s, ∑ j ∈ s, (g i - g j) ^ 2

Pairwise-difference form of the unnormalized variance of a function on a finite set.

theorem LeanPool.ErdosMoser.strictMonoFinNatLeDiff {m : ℕ} {g : Fin m → ℕ} (hg : StrictMono g) {i j : Fin m} (h : i ≤ j) : ↑j - ↑i ≤ g j - g i

A strictly increasing natural-valued sequence grows by at least the difference of its indices.

theorem LeanPool.ErdosMoser.strictMonoFinNatDiffSquareGe {m : ℕ} {g : Fin m → ℕ} (hg : StrictMono g) (i j : Fin m) : (↑↑i - ↑↑j) ^ 2 ≤ (↑(g i) - ↑(g j)) ^ 2

Increasing a collection of distinct natural numbers can only increase each squared pairwise difference from that of consecutive indices.

theorem LeanPool.ErdosMoser.varianceLowerBoundFinsetNat (T : Finset ℕ) : ↑T.card ^ 2 * (↑T.card ^ 2 - 1) / 12 ≤ ↑T.card * ∑ t ∈ T, ↑t ^ 2 - (∑ t ∈ T, ↑t) ^ 2

Among finite sets of natural numbers of a fixed cardinality, an initial interval minimizes the unnormalized empirical variance.