Exact variance of finite indicator losses #

This module records the elementary but useful variance identity behind the finite PAC-Bayes--Bernstein route. For an arbitrary Boolean-valued bad-event predicate on a finite data domain, the associated indicator loss has exact population variance R * (1 - R), where R is its population risk.

The result is distribution-generic within the finite setting: it assumes only a finite probability mass function. It is not restricted to a literal Bernoulli sample space or a particular classifier representation.

source

def FormalSLT.PACBayes.IndicatorVariance.indicatorLoss {ι : Type u_1} {Z : Type u_2} (bad : ι → Z → Bool) :

ι → Z → ℝ

The real-valued indicator loss associated with a Boolean bad-event predicate.

Equations

FormalSLT.PACBayes.IndicatorVariance.indicatorLoss bad i z = if bad i z = true then 1 else 0

Instances For

source

def FormalSLT.PACBayes.IndicatorVariance.indicatorPopulationRisk {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (bad : ι → Z → Bool) (i : ι) :

ℝ

Population risk of a Boolean indicator loss under a finite mass function.

Equations

FormalSLT.PACBayes.IndicatorVariance.indicatorPopulationRisk p bad i = FormalSLT.PACBayesFiniteProductMGF.finitePopulationRisk p (FormalSLT.PACBayes.IndicatorVariance.indicatorLoss bad) i

Instances For

source

@[simp]

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorLoss_sq {ι : Type u_1} {Z : Type u_2} (bad : ι → Z → Bool) (i : ι) (z : Z) :

indicatorLoss bad i z ^ 2 = indicatorLoss bad i z

source

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorLoss_nonneg {ι : Type u_1} {Z : Type u_2} (bad : ι → Z → Bool) (i : ι) (z : Z) :

0 ≤ indicatorLoss bad i z

source

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorLoss_le_one {ι : Type u_1} {Z : Type u_2} (bad : ι → Z → Bool) (i : ι) (z : Z) :

indicatorLoss bad i z ≤ 1

source

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorPopulationRisk_nonneg {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (bad : ι → Z → Bool) (i : ι) :

0 ≤ indicatorPopulationRisk p bad i

source

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorPopulationRisk_le_one {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (bad : ι → Z → Bool) (i : ι) :

indicatorPopulationRisk p bad i ≤ 1

source

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorPopulationRisk_mem_Icc {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (bad : ι → Z → Bool) (i : ι) :

indicatorPopulationRisk p bad i ∈ Set.Icc 0 1

source

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorDeviation_centered {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (bad : ι → Z → Bool) (i : ι) :

∑ z : Z, p z * (indicatorPopulationRisk p bad i - indicatorLoss bad i z) = 0

The population-centered indicator loss has mean zero.

source

theorem FormalSLT.PACBayes.IndicatorVariance.indicatorDeviation_secondMoment_eq {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (hp : PACBayesKL.IsPMF p) (bad : ι → Z → Bool) (i : ι) :

∑ z : Z, p z * (indicatorPopulationRisk p bad i - indicatorLoss bad i z) ^ 2 = indicatorPopulationRisk p bad i * (1 - indicatorPopulationRisk p bad i)

Exact variance identity for an arbitrary finite Boolean indicator loss.