[SamuelSchlesinger]

Proves McAllester's PAC-Bayes bound (SSBD Theorem 31.1) and its Occam corollary (SSBD Exercise 31.2) for a prior fixed before the sample over a countable hypothesis index, with losses in [0, 1]. With probability at least 1 − δ over m ≥ 2 i.i.d. examples, every posterior Q with KL(Q‖P) < ∞ satisfies

𝔼_Q L_D ≤ 𝔼_Q L_S + √((KL(Q‖P) + log(m/δ)) / (2(m−1))).

Builds on #4937 (true and empirical risk for general losses), which has landed; main is merged in.

What changed

Mathematical progress (CslibFrontier/MachineLearning/PACBayes/Basic.lean):

• measure_pi_exists_integral_risk_gt: the bound with log(√m/δ). The exponential moment from Hoeffding's lemma is at most √m, sharper than the m of SSBD Exercise 31.1.
• measure_pi_exists_integral_risk_gt_log_div: SSBD's log(m/δ) form, derived from the previous theorem.
• measure_pi_exists_risk_gt: point-mass posteriors give the Occam bound with log(1/P{i}).

Each bound is stated in the library's usual way: the measure of the bad samples, the set on which some posterior violates the bound, is at most δ. The posterior is quantified inside that event, so it may depend on the sample.

General probability infrastructure (drafted by worker pacbayes):

• Probability/ChangeOfMeasure.lean: integral_le_toReal_klDiv_add_log_integral_exp (Donsker–Varadhan, through Mathlib's tilted measure), klDiv_dirac_ne_top, toReal_klDiv_dirac.
• Probability/SubGaussian.lean: the exp(sX²) moment of a sub-Gaussian variable, and sub-Gaussianity of the centred empirical mean of [0, 1] variables. I found neither in Mathlib.

Probability/Pinsker.lean now derives its Gibbs step from the change-of-measure lemma, which makes it the lemma's first client. LossMinimization/Basic.lean (#4937) gains public measurable_empiricalRisk, trueRisk_mem_Icc and empiricalRisk_mem_Icc.

The PR also adds tests (CslibFrontierTests/PACBayes.lean), the pac-bayes-mcallester results entry, a manual section, and bib entries DonskerVaradhan1983 and McAllester1999. Risks reuse trueRisk/empiricalRisk from #4937.

Limitations

• The hypothesis index is countable with measurable singletons; SSBD also allows densities.
• Each loss ℓ i must be measurable, and m ≥ 2 is required. At m = 1 the margin divides by 2(m − 1) = 0 and vanishes, and a test exhibits a sample of probability 1/2 that violates the bound.
• Posteriors with KL = ∞ are excluded; the source's bound is vacuous for them.

The broader objective of #4916 stays open: measurable hypothesis spaces, the Maurer–Seeger kl form, Catoni-style bounds, and margin applications.

Validation

• Before rebasing onto feat(MachineLearning): true and empirical risk for general losses #4937, scripts/check.sh --quick fell back to the full check, and every gate passed: build, test, lint, mk_all, lint-style, checkInitImports, hygiene, ratchets, doc pins, result registry. I stopped only the final step, which re-elaborates cache-restored outputs and was taking hours; CI covers it.
• After merging main at 269ed43: --wfail builds of LossMinimization, Pinsker, Divergence, ProbabilityToolkit2, the LossMinimization tests, PACBayes and its tests, and Entries; mk_all --check, check_hygiene, lint-style and check_operator_manual pass.
• Earlier, after the rebase and squash: lake build --wfail --iofail on the new modules, the tests and CslibFrontierResults.Entries; lake lint on the module; check_hygiene.py --check-simp; lake exe mk_all --check; lint-style; check_operator_manual.py.
• CI provides the full run.

Manual impact

• Operator's Manual: added the "PAC-Bayes bounds" section to the learning chapter, linking the modules and tests.
• Agent Operator's Manual: no edit needed; the workflow is unchanged.
• No ROADMAP edit, per the issue.

Part of #4916.

AI disclosure: implemented by a Jetski AI agent as worker pacbayes-2 (continuing worker pacbayes) under coordinator session 5f40c2da. Agent review is not human review.

[SamuelSchlesinger]

Reviewer review-b (Jetski swarm, coordinator session 5f40c2da; non-author agent review, not human review) at 408d354 (top commit only; base #4937 not reviewed): CHANGES REQUESTED

The mathematics is right, and the statements match SSBD Theorem 31.1 (p. 416, proof pp. 416–417) and Exercise 31.2 (pp. 417–418). The setup is a countable index with measurable singletons, a prior P fixed before the sample, measurable losses in [0, 1], m ≥ 2 and δ > 0 (the source's δ < 1 is not needed). The bad event says that some posterior Q with klDiv Q P ≠ ⊤ violates the bound, so Q may depend on S, as in the source. The steps check out:

• Change of measure via the tilted measure.
• Jensen via variance_nonneg.
• Tonelli plus Markov at √m/δ.
• The √m moment: Hoeffding's lemma gives proxy 1/(4m) for the empirical mean, and the Gaussian-integral bound 1/√(1 − 2sc) at s = 2(m−1) gives exactly √m. That is sharper than Exercise 31.1's m.

The Dirac KL lemma gives log(1/P{i}). The tests are concrete and nonvacuous: at m = 1024, δ = 1/16 they show both constants have empirical risk ≥ 2/5 w.p. ≥ 15/16. They also include an infinite-KL posterior and the m = 1 counterexample to dropping m ≥ 2. I found no existing Mathlib or library lemma for the exp(sX²) moment, sub-Gaussianity of a Measure.pi empirical mean, or the Dirac KL. Reusing Mathlib's klDiv and HasSubgaussianMGF is right.

Requested

1. Derive the change-of-measure argument once. Probability/Pinsker.lean:75–82 (main) does the same Gibbs-for-ν.tilted step inline: integral_llr_add_sub_measure_univ_nonneg, then integral_llr_tilted_right. integral_le_toReal_klDiv_add_log_integral_exp (ChangeOfMeasure.lean:57) now packages exactly that step. Please derive ofReal_two_mul_sq_measureReal_sub_le_klDiv's hgibbs from the new lemma (at f = t • X), so Pinsker becomes its first client (AGENTS "Placement and reuse": derive a substantial shared argument once).
2. Don't hide public-API facts. measurable_empiricalRisk (Basic.lean:76), risk_mem_Icc (l. 187) and empiricalRisk_mem_Icc (l. 198) are stated purely in terms of the public trueRisk/empiricalRisk, and any client of #4937 will want them (CONTRIBUTING "Public surface": bounds and measurability stay public). Please make them public in Cslib.MachineLearning, ideally in LossMinimization/Basic.lean (this commit may touch it). Rename risk_mem_Icc to trueRisk_mem_Icc and give it D/ℓ explicit names.

Nits (non-blocking)

3. SubGaussian.lean:161–170: the variance-proxy arithmetic needs two erws and alternates field_simp/simp only. A separate have computing (1/m)^2 * ∑ i, (‖1 - 0‖₊/2)^2 = (4m)⁻¹ in ℝ≥0 (via NNReal.eq; push_cast; field_simp), followed by convert … using 2, would be sturdier.
4. Results topic := "learning theory". main has only "online learning", #4941 uses "statistical learning", and #4948 uses "learning theory". Please settle on one string.
5. The manual section is inserted at the same anchor (after "Agnostic PAC learning") as #4941's SRM section, so expect a trivial conflict for whichever lands second. Once both land, a one-line cross-reference would help: for a countable class, #4941's weighted-SRM/MDL bound √((log(1/w h) + log(2/δ))/(2m)) is the sharper Occam form for the 0-1 loss, while this PR covers general [0, 1] losses.
6. PACBayes test l. 108–110: "which has probability 1/2 under noisy" is asserted but not checked. Fine as commentary.

Manuals: the Operator's Manual section is accurate and links the modules and the test. The Agent Operator's Manual needs no edit, which I agree with. Bib entries are in key order. The CI advisory notices will be checked on the fix head, since ci-checks is still pending here.

[SamuelSchlesinger]

Fixed in 4b424e1, a new commit on top, so the history is not rewritten.

1. Pinsker's hgibbs now comes from integral_le_toReal_klDiv_add_log_integral_exp. It splits on klDiv μ ν = ⊤ and then uses ofReal_le_iff_le_toReal. The statement is unchanged.
2. measurable_empiricalRisk, trueRisk_mem_Icc (renamed, with ℓ and D explicit) and empiricalRisk_mem_Icc are now public in Cslib.MachineLearning in LossMinimization/Basic.lean. They take per-hypothesis assumptions (hℓ : ∀ z, ℓ w z ∈ Icc 0 1). trueRisk_mem_Icc uses integral_mono_of_nonneg, so it no longer needs measurability. The module docstring and the manual's general-losses paragraph list them.
3. The proxy arithmetic is now a separate have hc. It is stated with .mk as in Mathlib's const_mul, because the anonymous constructor elaborates at {r // 0 ≤ r}. The proof is simp only/ext1/push_cast/field_simp/ring, with no erw.
4. The topic is now "statistical learning", to match feat(MachineLearning): nonuniform learnability, SRM and MDL bound #4941, feat(MachineLearning): AdaBoost and its training-error bound #4948 and feat(MachineLearning): replace-one stability and regularized loss minimization #4940.
5. I'll add the SRM cross-reference, and resolve the manual conflict if there is one, when feat(MachineLearning): nonuniform learnability, SRM and MDL bound #4941 and this PR are both in.
6. Left as commentary.

Rebuilt with --wfail: Pinsker, Divergence, ProbabilityToolkit2, the LossMinimization tests, PACBayes and its tests, and Entries. lake lint passes on the changed modules, and check_hygiene, lint-style, mk_all --check and check_operator_manual pass.

[SamuelSchlesinger]

Reviewer review-b (Jetski swarm, coordinator session 5f40c2da; non-author agent review, not human review) at 4b424e1 (top two commits; base #4937 not reviewed by me): APPROVE

This reviews the delta from 408d354 against my earlier review. Held: the PR is stacked on #4937, which has not landed. I'll confirm ci-checks and its advisory notices at this head.

1. Resolved. Pinsker's hgibbs is now integral_le_toReal_klDiv_add_log_integral_exp hkl hfμ hexp. The klDiv = ⊤ case is a terminal simp, and the finite case goes through ENNReal.ofReal_le_iff_le_toReal. The rest of the proof (Hoeffding plus nlinarith) is unchanged, so Pinsker is now a client of the change-of-measure lemma. Pinsker.lean imports ChangeOfMeasure with a plain import, which is correct for a proof-only dependency.
2. Resolved. empiricalRisk_mem_Icc, trueRisk_mem_Icc and measurable_empiricalRisk are now public in LossMinimization/Basic.lean, with the docstring list and manual updated. trueRisk_mem_Icc dropped the measurability hypothesis via integral_mono_of_nonneg; it is correct for any probability measure. Note that this commit edits #4937's file, so a later change to #4937 will need a restack here.
3. Resolved. The SubGaussian variance-proxy constant is now a separate hc without erw.
4. Resolved: topic := "statistical learning".
5. Waits for #4941, which is fine.

No new findings.

[SamuelSchlesinger]

Reviewer review-b (Jetski swarm, coordinator session 5f40c2da; non-author agent review, not human review) at 4c233cf: APPROVE (merge resolution after #4937 landed)

The merge of main (269ed43, which includes #4937) into the approved head 4b424e1 is correct.

• I ran check_restack.py --approved-base 2c69c2f651 4b424e1bb6 4c233cf…. It reports differences only in the two conflicted files, and both are union resolutions:
  • CslibFrontierResults/Entries.lean: the PACBayes.Basic import and the pac-bayes-mcallester entry are kept unchanged, after main's srm-nonuniform-learnability/mdl-bound.
  • learning-and-testing.md: the PAC-Bayes section is kept after main's "Nonuniform learning, SRM and MDL" section.
• The one new sentence is the SRM/MDL cross-reference (my earlier nit 5), and it is accurate. Applied to singleton classes with weights w h, Weighting.measure_pi_exists_lt_error_le gives √((log (1 / w h) + log (2 / δ)) / (2 m)) for the 0-1 loss. That is sharper than the Occam corollary's √((log (1 / P {i}) + log (m / δ)) / (2 (m - 1))). The anchor #nonuniform-learning-srm-and-mdl matches the heading.
• LossMinimization/Basic.lean has the same patch-id against main as the approved head had against 2c69c2f. The other Lean files, the tests and references.bib replay cleanly.
• No conflict markers remain, and git diff origin/main... shows exactly this PR's 10 files.
• I merged this head with the queued #5010 in a scratch merge-tree, and it merges cleanly.

I'll queue once ci-checks passes at this head.