Finite PAC-Bayes Bernstein confidence bounds for indicator losses

This module closes the finite indicator-loss Bernstein chain. It combines the exact variance identity, the finite-product MGF, the prior-averaged normalized moment, and the finite PAC-Bayes change-of-measure adapter.

For a finite hypothesis class and a full-support prior, the main theorem bounds the product-law mass of samples on which some posterior violates the explicit fixed-tilt Bernstein inequality. Thus the bound holds simultaneously for all finite posteriors outside a bad set of mass at most delta.

The result is finite, i.i.d., fixed-sample, fixed-tilt, and uses population Bernoulli variance R_i * (1 - R_i) / n. It is not empirical Bernstein, continuous-hypothesis, time-uniform, or optimized over the tilt.

Mathematical sources: Boucheron, Lugosi, and Massart (2013), Concentration Inequalities, for the Bernstein MGF route; Donsker and Varadhan (1975) for the change-of-measure principle; and Tolstikhin and Seldin (2013), "PAC-Bayes-Empirical-Bernstein Inequality," for the variance-sensitive PAC-Bayes context.

noncomputable def FormalSLT.PACBayes.IndicatorBernsteinConfidence.indicatorFinitePACBayesBernsteinBadSamples {ι : Type u_1} {Z : Type u_2} [Fintype ι] [Fintype Z] (n : ℕ) (p : Z → ℝ) (π : ι → ℝ) (bad : ι → Z → Bool) (lambda delta : ℝ) : Finset (Fin n → Z)

Samples on which some finite posterior violates the indicator-specialized fixed-tilt PAC-Bayes Bernstein inequality.

Equations

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

theorem FormalSLT.PACBayes.IndicatorBernsteinConfidence.indicator_posteriorGeneralizationGap_le_of_not_mem {ι : Type u_1} {Z : Type u_2} [Fintype ι] [Fintype Z] (n : ℕ) (p : Z → ℝ) (π : ι → ℝ) (bad : ι → Z → Bool) (lambda delta : ℝ) (S : Fin n → Z) (hS : S ∉ indicatorFinitePACBayesBernsteinBadSamples n p π bad lambda delta) (ρ : ι → ℝ) (hρ : PACBayesKL.IsPMF ρ) : (PACBayesKL.posteriorGeneralizationGap ρ (IndicatorVariance.indicatorPopulationRisk p bad) fun (i : ι) => PACBayesFiniteProductMGF.finiteEmpiricalRisk (IndicatorVariance.indicatorLoss bad) i S) ≤ (PACBayesKL.klDiv ρ π + Real.log (1 / delta)) / lambda + lambda * PACBayesBernstein.posteriorMarginVarianceProxy ρ (IndicatorBernsteinMoment.indicatorBernsteinVarianceProxy n p bad) / (2 * (1 - IndicatorBernsteinMoment.indicatorBernsteinScale n * lambda))

Outside the specialized bad-sample set, every finite posterior satisfies the explicit indicator PAC-Bayes Bernstein inequality.

theorem FormalSLT.PACBayes.IndicatorBernsteinConfidence.indicator_finitePACBayesBernstein_fixedLambda_badEventMass_le_delta {ι : Type u_1} {Z : Type u_2} [Fintype ι] [Nonempty ι] [Fintype Z] {n : ℕ} (hn : 0 < n) (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) {π : ι → ℝ} (hπ : PACBayesKL.IsFullSupportPMF π) (bad : ι → Z → Bool) (lambda delta : ℝ) (hlambda : 0 < lambda) (hlambda_lt : lambda < 3 * ↑n) (hdelta : 0 < delta) : ∑ S ∈ indicatorFinitePACBayesBernsteinBadSamples n p π bad lambda delta, PACBayesFiniteProductMGF.finiteProductSampleWeight p S ≤ delta

Finite i.i.d. PAC-Bayes Bernstein confidence theorem for indicator losses.

Under a finite data PMF and full-support finite prior, the product-law mass of samples on which any posterior violates the fixed-lambda Bernstein bound is at most delta. The scale is 1/(3n) and the per-hypothesis variance proxy is the exact Bernoulli quantity R_i * (1 - R_i) / n.