Variance of distinct subset sums

This file proves the first and second moment identities for subset sums and combines them with the discrete variance bound to obtain Leo Moser's exact finite sum-of-squares inequality.

theorem LeanPool.ErdosMoser.sumSubsetSums (B : Finset ℕ) (f : ℕ → ℝ) : 2 * ∑ T ∈ B.powerset, ∑ i ∈ T, f i = 2 ^ B.card * ∑ i ∈ B, f i

Twice the sum of all subset sums is 2 ^ |B| times the sum of the elements of B.

theorem LeanPool.ErdosMoser.secondMomentSubsetSums (B : Finset ℕ) (f : ℕ → ℝ) : 4 * ∑ S ∈ B.powerset, (∑ i ∈ S, f i) ^ 2 = 2 ^ B.card * (∑ i ∈ B, f i ^ 2 + (∑ i ∈ B, f i) ^ 2)

Exact second-moment identity for the subset sums of a finite set.

theorem LeanPool.ErdosMoser.varianceIdentitySubsetSums (B : Finset ℕ) (f : ℕ → ℝ) : 4 * ∑ S ∈ B.powerset, (∑ i ∈ S, f i) ^ 2 - 2 ^ B.card * (∑ i ∈ B, f i) ^ 2 = 2 ^ B.card * ∑ i ∈ B, f i ^ 2

Algebraic variance identity for subset sums.

theorem LeanPool.ErdosMoser.imageSubsetSumsCard {A : Finset ℕ} (h : HasDistinctSubsetSums A) : (Finset.image (fun (S : Finset ℕ) => S.sum id) A.powerset).card = 2 ^ A.card

The image of the subset-sum map has cardinality 2 ^ A.card when the subset sums of A are distinct.

theorem LeanPool.ErdosMoser.leoMoserVarianceBound {A : Finset ℕ} (h : HasDistinctSubsetSums A) : 4 ^ A.card - 1 ≤ 3 * ∑ a ∈ A, ↑a ^ 2

Leo Moser's finite variance inequality. If a finite set of natural numbers has distinct subset sums, then 4 ^ |A| - 1 ≤ 3 * ∑ a ∈ A, a ^ 2.

This is Theorem 2 of Richard K. Guy's 1982 account, where it is attributed to Leo Moser.