Finite empirical-variance exponential moments

This module proves a finite, source-normalized lower-tail MGF inequality for the Bessel-corrected empirical variance of a bounded loss. The proof uses a sharp single-pair chord bound, exact factorization over disjoint random-matching blocks, and finite Jensen over all coordinate permutations.

For every sample size n ≥ 2, the final theorem matches the coefficient in Tolstikhin and Seldin (2013), equation (9):

E exp(eta * n * (V - Vhat)) ≤ exp(eta^2 * n^2 * V / (2 * (n - 1))).

The intermediate matching theorem is sharper when n is even. These are fixed-hypothesis finite-product moment bounds; no PAC-Bayes change of measure or posterior-uniform confidence statement is claimed here.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.pairVarianceKernel_mem_Icc {ι : Type u_1} {Z : Type u_2} (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) (z w : Z) : FiniteEmpiricalVarianceMatching.pairVarianceKernel ℓ i z w ∈ Set.Icc 0 (1 / 2)

For [0,1]-valued losses, the pair-variance kernel lies in [0,1/2].

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.pairVarianceKernel_lowerTailMGF {ι : 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) {t : ℝ} (ht : 0 ≤ t) : ∑ z : Z, ∑ w : Z, p z * p w * Real.exp (t * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVarianceMatching.pairVarianceKernel ℓ i z w)) ≤ Real.exp (t ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / 4)

Sharp single-pair lower-tail MGF. The kernel range is [0,1/2], which improves the quadratic coefficient from 1/2 to 1/4.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finitePairBlocks_lowerTailMGF {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {m : ℕ} (hm : 0 < m) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) {lam : ℝ} (hlam : 0 ≤ lam) : ∑ S : Fin m → Fin 2 → Z, ∏ r : Fin m, PACBayesFiniteProductMGF.finiteProductSampleWeight p (S r) * Real.exp (lam / ↑m * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVarianceMatching.pairVarianceKernel ℓ i (S r 0) (S r 1))) ≤ Real.exp (lam ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / (4 * ↑m))

Sharp lower-tail MGF for the mean of m independent pair kernels.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finitePairBlockMean_lowerTailMGF {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {m : ℕ} (hm : 0 < m) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) {lam : ℝ} (hlam : 0 ≤ lam) : ∑ S : Fin m → Fin 2 → Z, FiniteEmpiricalVarianceMatching.finitePairBlockSampleWeight p S * Real.exp (lam * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVarianceMatching.finitePairBlockMean ℓ i S)) ≤ Real.exp (lam ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / (4 * ↑m))

Natural centered-MGF form of the independent-pair result.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finitePairBlockMean_withRemainder_lowerTailMGF {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {m r : ℕ} (hm : 0 < m) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) {lam : ℝ} (hlam : 0 ≤ lam) : ∑ S : Fin m → Fin 2 → Z, ∑ U : Fin r → Z, FiniteEmpiricalVarianceMatching.finitePairBlockSampleWeight p S * PACBayesFiniteProductMGF.finiteProductSampleWeight p U * Real.exp (lam * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVarianceMatching.finitePairBlockMean ℓ i S)) ≤ Real.exp (lam ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / (4 * ↑m))

Unused iid coordinates integrate out exactly. This is the odd-sample bridge: instantiate r = 1.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finiteCanonicalPairMean_lowerTailMGF {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {m r : ℕ} (hm : 0 < m) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) {lam : ℝ} (hlam : 0 ≤ lam) : ∑ T : Fin (m * 2 + r) → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p T * Real.exp (lam * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVarianceMatching.finiteCanonicalPairMean ℓ i T)) ≤ Real.exp (lam ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / (4 * ↑m))

The sharp pair-block MGF transported back to an ordinary Fin-indexed iid sample, allowing r unused coordinates.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.exp_population_sub_sampleVariance_le_permAverage {ι : Type u_1} {Z : Type u_2} {m r : ℕ} (hm : 0 < m) (ℓ : ι → Z → ℝ) (i : ι) (T : Fin (m * 2 + r) → Z) (V lam : ℝ) : Real.exp (lam * (V - Statistics.ClassicalEstimation.sampleVarianceBessel fun (k : Fin (m * 2 + r)) => ℓ i (T k))) ≤ (∑ σ : Equiv.Perm (Fin (m * 2 + r)), Real.exp (lam * (V - FiniteEmpiricalVarianceMatching.finiteCanonicalPairMean ℓ i fun (k : Fin (m * 2 + r)) => T (σ k)))) / ↑(Fintype.card (Equiv.Perm (Fin (m * 2 + r))))

Finite Jensen bounds the exponential centered at the sample variance by the uniform average over permuted canonical matchings.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.permutedCanonicalPairMean_lowerTailMGF {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {m r : ℕ} (hm : 0 < m) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) {lam : ℝ} (hlam : 0 ≤ lam) (σ : Equiv.Perm (Fin (m * 2 + r))) : ∑ T : Fin (m * 2 + r) → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p T * Real.exp (lam * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVarianceMatching.finiteCanonicalPairMean ℓ i ((FiniteEmpiricalVarianceMatching.samplePrecompPerm σ Z) T))) ≤ Real.exp (lam ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / (4 * ↑m))

Every permuted canonical matching has the same product-law MGF bound as the canonical matching.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finiteEmpiricalVariance_lowerTailMGF_randomMatching {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {m r : ℕ} (hm : 0 < m) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) {lam : ℝ} (hlam : 0 ≤ lam) : ∑ T : Fin (m * 2 + r) → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p T * Real.exp (lam * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVariance.finiteEmpiricalVariance ℓ i T)) ≤ Real.exp (lam ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / (4 * ↑m))

Full sample-variance lower-tail MGF obtained by random matching and finite Jensen.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finiteEmpiricalVariance_lowerTailMGF_randomMatching_scaled {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {m r : ℕ} (hm : 0 < m) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ℓ : ι → Z → ℝ) (i : ι) (hℓ : ∀ (z : Z), ℓ i z ∈ Set.Icc 0 1) {lam : ℝ} (hlam : 0 ≤ lam) : ∑ T : Fin (m * 2 + r) → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p T * Real.exp (lam * ↑(m * 2 + r) * (FiniteEmpiricalVariance.finitePopulationVariance p ℓ i - FiniteEmpiricalVariance.finiteEmpiricalVariance ℓ i T)) ≤ Real.exp (lam ^ 2 * ↑(m * 2 + r) ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ℓ i / (4 * ↑m))

n-scaled form. With m = floor(n/2) this is the Tolstikhin--Seldin coefficient n²/(4m).

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finiteEmpiricalVariance_lowerTailMGF_tolstikhinSeldin {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {n : ℕ} (hn : 2 ≤ n) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ell : ι → Z → ℝ) (i : ι) (hell : ∀ (z : Z), ell i z ∈ Set.Icc 0 1) {eta : ℝ} (heta : 0 ≤ eta) : ∑ S : Fin n → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p S * Real.exp (eta * ↑n * (FiniteEmpiricalVariance.finitePopulationVariance p ell i - FiniteEmpiricalVariance.finiteEmpiricalVariance ell i S)) ≤ Real.exp (eta ^ 2 * ↑n ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ell i / (2 * (↑n - 1)))

Source-normalized finite version of Tolstikhin--Seldin (2013), Eq. (9). The Bessel empirical variance is averaged under the explicit finite iid product law.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceMGF.finiteEmpiricalVariance_normalizedLowerTailMGF_le_one {ι : Type u_1} {Z : Type u_2} [Fintype Z] [DecidableEq Z] {n : ℕ} (hn : 2 ≤ n) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (ell : ι → Z → ℝ) (i : ι) (hell : ∀ (z : Z), ell i z ∈ Set.Icc 0 1) {eta : ℝ} (heta : 0 ≤ eta) : ∑ S : Fin n → Z, PACBayesFiniteProductMGF.finiteProductSampleWeight p S * Real.exp (eta * ↑n * (FiniteEmpiricalVariance.finitePopulationVariance p ell i - FiniteEmpiricalVariance.finiteEmpiricalVariance ell i S) - eta ^ 2 * ↑n ^ 2 * FiniteEmpiricalVariance.finitePopulationVariance p ell i / (2 * (↑n - 1))) ≤ 1

Normalized form of the source-facing empirical-variance MGF.

The deterministic variance penalty is moved inside the exponential, so the finite-product expectation is at most one. This is the form consumed by the finite PAC-Bayes change-of-measure layer.