Documentation

FormalSLT.PACBayes.FinitePMFBridge

Finite PAC-Bayes interoperability with mathlib probability measures #

This module connects FormalSLT's finite real-valued probability mass functions, posterior averages, and KL divergence to mathlib's PMF, Measure, and InformationTheory.klDiv APIs.

The KL bridge requires the posterior support to be contained in the prior support. This is exactly the finite absolute-continuity condition. Without it, FormalSLT's totalized real-valued finite sum is not the same object as mathlib's extended-real KL divergence, which is infinite when absolute continuity fails.

Real-valued PMFs as mathlib PMFs #

source
noncomputable def FormalSLT.PACBayesKL.IsPMF.toPMF {ι : Type u_1} [Fintype ι] {ρ : ι → ℝ} (hρ : IsPMF ρ) :
PMF ι

Convert a finite nonnegative real-valued PMF into mathlib's PMF type.

Equations
Instances For
    source
    @[simp]
    theorem FormalSLT.PACBayesKL.IsPMF.toPMF_apply {ι : Type u_1} [Fintype ι] {ρ : ι → ℝ} (hρ : IsPMF ρ) (i : ι) :
    hρ.toPMF i = ENNReal.ofReal (ρ i)
    source
    @[simp]
    theorem FormalSLT.PACBayesKL.IsPMF.toPMF_apply_toReal {ι : Type u_1} [Fintype ι] {ρ : ι → ℝ} (hρ : IsPMF ρ) (i : ι) :
    (hρ.toPMF i).toReal = ρ i

    Posterior averages as Bochner integrals #

    source
    theorem FormalSLT.PACBayesKL.IsPMF.integral_toPMF_eq_sum {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ : ι → ℝ} (hρ : IsPMF ρ) (g : ι → ℝ) :
    ∫ (i : ι), g i ∂hρ.toPMF.toMeasure = ∑ i : ι, ρ i * g i

    Integration against the mathlib PMF associated to a FormalSLT finite PMF is the corresponding finite weighted sum.

    source
    theorem FormalSLT.PACBayesKL.integral_toPMF_eq_posteriorAverage {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ : ι → ℝ} (hρ : IsPMF ρ) (g : ι → ℝ) :
    ∫ (i : ι), g i ∂hρ.toPMF.toMeasure = posteriorAverage ρ g

    A FormalSLT finite posterior average is the Bochner integral against the corresponding mathlib probability measure.

    Support-aware measure and KL bridges #

    source
    theorem FormalSLT.PACBayesKL.toPMF_toMeasure_absolutelyContinuous_of_support {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ π : ι → ℝ} (hρ : IsPMF ρ) (hπ : IsPMF π) (hsupport : Function.support ρ ⊆ Function.support π) :
    hρ.toPMF.toMeasure.AbsolutelyContinuous hπ.toPMF.toMeasure

    Finite support inclusion induces absolute continuity between the associated mathlib probability measures.

    source
    theorem FormalSLT.PACBayesKL.toPMF_toMeasure_absolutelyContinuous_of_fullSupport {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ π : ι → ℝ} (hρ : IsPMF ρ) (hπ : IsFullSupportPMF π) :
    hρ.toPMF.toMeasure.AbsolutelyContinuous ⋯.toPMF.toMeasure

    A full-support prior dominates every finite posterior PMF.

    source
    theorem FormalSLT.PACBayesKL.klDiv_nonneg_of_support {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ π : ι → ℝ} (hρ : IsPMF ρ) (hπ : IsPMF π) (hsupport : Function.support ρ ⊆ Function.support π) :
    0 ≤ klDiv ρ π

    FormalSLT's finite KL sum is nonnegative under the minimal finite absolute-continuity assumption.

    source
    theorem FormalSLT.PACBayesKL.informationTheory_klDiv_toPMF_eq_of_support {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ π : ι → ℝ} (hρ : IsPMF ρ) (hπ : IsPMF π) (hsupport : Function.support ρ ⊆ Function.support π) :
    InformationTheory.klDiv hρ.toPMF.toMeasure hπ.toPMF.toMeasure = ENNReal.ofReal (klDiv ρ π)

    Under finite support inclusion, mathlib's extended-real KL divergence is exactly ENNReal.ofReal of FormalSLT's finite KL sum.

    source
    theorem FormalSLT.PACBayesKL.toReal_informationTheory_klDiv_toPMF_eq_of_support {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ π : ι → ℝ} (hρ : IsPMF ρ) (hπ : IsPMF π) (hsupport : Function.support ρ ⊆ Function.support π) :
    (InformationTheory.klDiv hρ.toPMF.toMeasure hπ.toPMF.toMeasure).toReal = klDiv ρ π

    Real-valued form of the support-aware finite KL interoperability theorem.

    source
    theorem FormalSLT.PACBayesKL.informationTheory_klDiv_toPMF_eq_of_fullSupport {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ π : ι → ℝ} (hρ : IsPMF ρ) (hπ : IsFullSupportPMF π) :
    InformationTheory.klDiv hρ.toPMF.toMeasure ⋯.toPMF.toMeasure = ENNReal.ofReal (klDiv ρ π)

    Full-support specialization of the extended-real finite KL bridge used by FormalSLT's finite PAC-Bayes theorems.

    source
    theorem FormalSLT.PACBayesKL.toReal_informationTheory_klDiv_toPMF_eq_of_fullSupport {ι : Type u_1} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] {ρ π : ι → ℝ} (hρ : IsPMF ρ) (hπ : IsFullSupportPMF π) :
    (InformationTheory.klDiv hρ.toPMF.toMeasure ⋯.toPMF.toMeasure).toReal = klDiv ρ π

    Full-support specialization of the real-valued finite KL bridge used by FormalSLT's finite PAC-Bayes theorems.