Finite empirical-variance foundations for PAC-Bayes

This module isolates the deterministic variance objects used by finite PAC-Bayes empirical-Bernstein arguments:

• the population variance of a hypothesis loss under a finite PMF;
• the Bessel-corrected empirical variance of the observed losses;
• the exact ordered off-diagonal pairwise representation of that empirical variance; and
• elementary [0, 1] bounds; and
• unbiasedness under the explicit finite iid product sample law.

Proof strategy: finite-sum algebra proves the deterministic identities; a coordinate-swap equivalence proves the finite-IID marginal identity; finite-sum reordering then proves unbiasedness.

The ordered representation is the finite U-statistic form

(2 n (n - 1))⁻¹ ∑ᵢ ∑_{j ≠ i} (xᵢ - xⱼ)².

Equivalently, it is (n (n - 1))⁻¹ times the sum over unordered pairs. This module does not prove an exponential-moment inequality, a confidence event, or a PAC-Bayes empirical-Bernstein theorem. The object is per hypothesis; it is not the variance of a posterior-averaged loss. Substantive sample-variance results assume n ≥ 2.

The normalization follows Tolstikhin and Seldin (2013), "PAC-Bayes-Empirical-Bernstein Inequality," equation (5). The ordered-pair identity is the equivalent second-order U-statistic representation used in the empirical-Bernstein literature; see also Maurer and Pontil (2009), "Empirical Bernstein Bounds and Sample Variance Penalization."

def FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePopulationVariance {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (ℓ : ι → Z → ℝ) (i : ι) : ℝ

Population variance of the loss of hypothesis i under a finite PMF.

Equations

• FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePopulationVariance p ℓ i = ∑ z : Z, p z * (ℓ i z - FormalSLT.PACBayesFiniteProductMGF.finitePopulationRisk p ℓ i) ^ 2

noncomputable def FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteEmpiricalVariance {ι : Type u_1} {Z : Type u_2} {n : ℕ} (ℓ : ι → Z → ℝ) (i : ι) (S : Fin n → Z) : ℝ

Bessel-corrected empirical variance of the losses observed in S.

The denominator is n - 1; substantive theorems below assume 2 ≤ n.

Equations

• FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteEmpiricalVariance ℓ i S = FormalSLT.Statistics.ClassicalEstimation.sampleVarianceBessel fun (k : Fin n) => ℓ i (S k)

def FormalSLT.PACBayes.FiniteEmpiricalVariance.orderedOffDiagonalSquaredDifference {n : ℕ} (x : Fin n → ℝ) : ℝ

Sum of squared differences over ordered, distinct sample-index pairs.

Equations

• FormalSLT.PACBayes.FiniteEmpiricalVariance.orderedOffDiagonalSquaredDifference x = ∑ k : Fin n, ∑ j ∈ Finset.univ.erase k, (x k - x j) ^ 2

noncomputable def FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePairwiseEmpiricalVariance {ι : Type u_1} {Z : Type u_2} {n : ℕ} (ℓ : ι → Z → ℝ) (i : ι) (S : Fin n → Z) : ℝ

Ordered-pair realization of the empirical-variance U-statistic.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePopulationVariance_nonneg {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) : 0 ≤ finitePopulationVariance p ℓ i

Population variance is nonnegative under a finite PMF.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePopulationVariance_eq_secondMoment_sub_riskSq {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) : finitePopulationVariance p ℓ i = ∑ z : Z, p z * ℓ i z ^ 2 - PACBayesFiniteProductMGF.finitePopulationRisk p ℓ i ^ 2

Population variance is the second moment minus the squared population risk.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePopulationRisk_mem_Icc_of_bounded {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) : PACBayesFiniteProductMGF.finitePopulationRisk p ℓ i ∈ Set.Icc 0 1

A finite [0,1]-valued loss has population risk in [0,1].

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePopulationVariance_le_quarter {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) : finitePopulationVariance p ℓ i ≤ 1 / 4

The population variance of a finite [0,1]-valued loss is at most 1/4.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteEmpiricalVariance_nonneg {ι : Type u_1} {Z : Type u_2} {n : ℕ} (hn : 2 ≤ n) (ℓ : ι → Z → ℝ) (i : ι) (S : Fin n → Z) : 0 ≤ finiteEmpiricalVariance ℓ i S

Bessel-corrected empirical variance is nonnegative for n ≥ 2.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.orderedOffDiagonalSquaredDifference_eq_two_mul_card_mul_centeredSum {n : ℕ} (hn : 0 < n) (x : Fin n → ℝ) : orderedOffDiagonalSquaredDifference x = 2 * ↑n * ∑ k : Fin n, (x k - Statistics.sampleMean x) ^ 2

The ordered off-diagonal squared-difference sum is twice n times the centered sum of squares.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteEmpiricalVariance_eq_pairwise {ι : Type u_1} {Z : Type u_2} {n : ℕ} (hn : 2 ≤ n) (ℓ : ι → Z → ℝ) (i : ι) (S : Fin n → Z) : finiteEmpiricalVariance ℓ i S = finitePairwiseEmpiricalVariance ℓ i S

Exact source-facing pairwise identity for the finite empirical variance.

The ordered sum counts each unordered pair twice, which accounts for the factor 2 in the denominator.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.orderedOffDiagonalSquaredDifference_le {n : ℕ} (hn : 2 ≤ n) (x : Fin n → ℝ) (hx : ∀ (k : Fin n), x k ∈ Set.Icc 0 1) : orderedOffDiagonalSquaredDifference x ≤ ↑n * (↑n - 1)

Ordered pairwise numerator bound for a sample taking values in [0,1].

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteEmpiricalVariance_le_card_div_pred_mul_empiricalRisk {ι : Type u_1} {Z : Type u_2} {n : ℕ} (hn : 2 ≤ n) (ℓ : ι → Z → ℝ) (i : ι) (S : Fin n → Z) (hℓ : ∀ (k : Fin n), ℓ i (S k) ∈ Set.Icc 0 1) : finiteEmpiricalVariance ℓ i S ≤ ↑n / (↑n - 1) * PACBayesFiniteProductMGF.finiteEmpiricalRisk ℓ i S

For samples whose observed losses lie in [0,1], empirical variance is at most n / (n - 1) times empirical risk. This is the deterministic comparison used in Tolstikhin--Seldin after their equation (7).

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteEmpiricalVariance_le_half {ι : Type u_1} {Z : Type u_2} {n : ℕ} (hn : 2 ≤ n) (ℓ : ι → Z → ℝ) (i : ι) (S : Fin n → Z) (hℓ : ∀ (k : Fin n), ℓ i (S k) ∈ Set.Icc 0 1) : finiteEmpiricalVariance ℓ i S ≤ 1 / 2

A Bessel-corrected empirical variance of [0,1] observations is at most 1/2.

Finite iid expectation identities

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteProductSampleWeight_pairExpectation {Z : Type u_2} {n : ℕ} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (k j : Fin n) (hkj : k ≠ j) (g : Z → Z → ℝ) : ∑ S : Fin n → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p S * g (S k) (S j) = ∑ z : Z, ∑ w : Z, p z * p w * g z w

Two distinct coordinates of a finite iid product sample have the expected product marginal.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finitePairVarianceKernelExpectation_eq_populationVariance {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) : ∑ z : Z, ∑ w : Z, p z * p w * ((ℓ i z - ℓ i w) ^ 2 / 2) = finitePopulationVariance p ℓ i

The expected independent-pair squared-difference kernel is the population variance.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteProductSampleWeight_pairSquaredDifferenceExpectation_eq {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (k j : Fin n) (hkj : k ≠ j) : ∑ S : Fin n → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p S * (ℓ i (S k) - ℓ i (S j)) ^ 2 = 2 * finitePopulationVariance p ℓ i

For two distinct sample coordinates, the expected squared loss difference is twice the population variance.

theorem FormalSLT.PACBayes.FiniteEmpiricalVariance.finiteEmpiricalVariance_unbiased_finiteProduct {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 2 ≤ n) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) : ∑ S : Fin n → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p S * finiteEmpiricalVariance ℓ i S = finitePopulationVariance p ℓ i

The Bessel-corrected empirical loss variance is unbiased under the finite iid product sample law.