PAC-Bayes generalization certificate - compiler output Cert_E

This file was generated by compiler/compile.py from compiler/specs/Cert_E.json. It is a machine-checkable finite PAC-Bayes bounded-loss certificate.

Instance statistics

• hypothesis class: Fin 16
• data domain: Fin 2
• sample size: n = 2000
• bounded loss width: B = 1
• prior: uniform
• posterior summary: uniform
• posterior KL recorded by the sweep: 0
• confidence delta: 0.1
• complexity budget used in Lean: 2.30258509299
• computed McAllester bound: 0.0239926295609

The certificate instantiates FormalSLT.PACBayesBoundedLoss.finiteMcAllesterBoundedComplexity_badEventMass_le_delta. It proves that the finite product-sample mass of samples admitting a posterior inside the stated complexity budget but violating the corresponding square-root PAC-Bayes bound is at most delta.

noncomputable def FormalSLT.PACBayes.Generated.Cert_E.dataLaw : Fin 2 → ℝ

Data law on the two-point data domain.

Equations

• FormalSLT.PACBayes.Generated.Cert_E.dataLaw z = if z = 0 then 1 / 2 else 1 / 2

noncomputable def FormalSLT.PACBayes.Generated.Cert_E.prior : Fin 16 → ℝ

Full-support prior over the finite hypothesis class.

Equations

• FormalSLT.PACBayes.Generated.Cert_E.prior x✝ = 1 / 16

def FormalSLT.PACBayes.Generated.Cert_E.loss : Fin 16 → Fin 2 → ℝ

Bounded zero-one loss pattern used for the generated classification spec.

Equations

• FormalSLT.PACBayes.Generated.Cert_E.loss x✝ z = if z = 0 then 0 else 1

def FormalSLT.PACBayes.Generated.Cert_E.sampleSize : ℕ

Sample size.

Equations

• FormalSLT.PACBayes.Generated.Cert_E.sampleSize = 2000

noncomputable def FormalSLT.PACBayes.Generated.Cert_E.delta : ℝ

Confidence parameter.

Equations

• FormalSLT.PACBayes.Generated.Cert_E.delta = 1 / 10

noncomputable def FormalSLT.PACBayes.Generated.Cert_E.complexityBound : ℝ

Concrete positive complexity budget for the generated McAllester shell.

Equations

• FormalSLT.PACBayes.Generated.Cert_E.complexityBound = 460517018599 / 200000000000

noncomputable def FormalSLT.PACBayes.Generated.Cert_E.computedBound : ℝ

Numeric square-root term appearing in the emitted certificate.

Equations

• FormalSLT.PACBayes.Generated.Cert_E.computedBound = √(FormalSLT.PACBayes.Generated.Cert_E.complexityBound / (2 * ↑FormalSLT.PACBayes.Generated.Cert_E.sampleSize))

theorem FormalSLT.PACBayes.Generated.Cert_E.dataLaw_isPMF : PACBayesKL.IsPMF dataLaw

dataLaw is a probability mass function.

theorem FormalSLT.PACBayes.Generated.Cert_E.prior_isFullSupportPMF : PACBayesKL.IsFullSupportPMF prior

prior is a full-support probability mass function.

theorem FormalSLT.PACBayes.Generated.Cert_E.loss_mem_unitInterval (i : Fin 16) (z : Fin 2) : 0 ≤ loss i z ∧ loss i z ≤ 1

Every generated loss entry lies in [0, 1].

theorem FormalSLT.PACBayes.Generated.Cert_E.cert_E_generalization_certificate : ∑ S : Fin sampleSize → Fin 2 with ∃ (ρ : Fin 16 → ℝ), PACBayesKL.IsPMF ρ ∧ PACBayesKL.klDiv ρ prior + Real.log (1 / delta) ≤ complexityBound ∧ PACBayesBoundedLoss.posteriorPopulationRisk dataLaw loss ρ > PACBayesBoundedLoss.posteriorEmpiricalRisk loss ρ S + computedBound, PACBayesFiniteProductMGF.finiteProductSampleWeight dataLaw S ≤ delta

Machine-checked PAC-Bayes certificate for Cert_E.