[SamuelSchlesinger]

Mistake bound ⇒ realizable PAC learning by online-to-batch conversion: the first milestone (Part A) of #4918.

Mathematical result. A deterministic OnlineLearner A with mistakeBound A C ≤ M gives a PAC learner over realizableDistributions C. Let prefixHypothesis A S t be A's hypothesis after the first t examples. On i.i.d. examples its expected error equals the probability that A errs on the fresh example t of an (m + 1)-sample (lintegral_error_prefixHypothesis_eq, via measurePreserving_piFinSuccAbove and Fubini). Summing over t ≤ m bounds the expected errors of the m + 1 prefix hypotheses by M (sum_lintegral_error_prefixHypothesis_le). This is the random-stopping conversion of Littlestone (COLT 1989) and Cesa-Bianchi–Conconi–Gentile (IEEE TIT 2004): a uniformly random prefix hypothesis has expected error ≤ M/(m+1). Upstream IsPACLearnerFor needs a deterministic learner, so the module derandomizes with the majority vote prefixMajority A, whose expected error is ≤ 2M/(m+1) (lintegral_error_prefixMajority_le). Markov then gives IsPACLearnerFor m ε δ C (realizableDistributions C) whenever 2M ≤ εδ(m+1) (isPACLearnerFor_prefixMajority), and IsPACLearnable with sample size ⌈2M/(εδ)⌉ (isPACLearnable_of_mistakeBound_le). On countable domains with measurable singletons, a finite optimalMistakeBound (equivalently finite Littlestone dimension) implies PAC learnability (isPACLearnable_of_optimalMistakeBound_ne_top).

Model and limitations.

• Measurability: Fubini needs the learner to be jointly measurable in history and instance for each history length (IsMeasurableLearner). This holds automatically on countable domains with measurable singletons (isMeasurableLearner_of_countable).
• The confidence dependence is 1/δ (Markov), not the log(1/δ) of Littlestone's hypothesis-testing conversion, which is not formalized.
• Source mapping: the M/(m+1) bound on the average over prefixes is the sources' statement. The majority vote and its factor 2 are this library's derandomization. Theorem numbers and locators are unverified and marked so.
• Learners are semantic maps. No running time is claimed.
• Not done here (remaining in Online-to-batch conversion: SGD excess-risk bound and mistake bounds to PAC learning #4918): Part B, convex online-to-batch in expectation and the SGD corollary. The mistake-bound ⇒ compression route is Sample compression schemes: the Littlestone–Warmuth bound and compression from mistake bounds #4914 (worker compression). It is not duplicated here.

Infrastructure: two references.bib entries (Littlestone1989, CesaBianchiConconiGentile2004).

Tests (CslibFrontierTests/OnlineToBatch.lean):

• A concrete majority vote of halving's prefix hypotheses whose first prefix hypothesis is outvoted.
• A 7-example (1/2, 1/2)-PAC learner for three concepts on Fin 2, and a proof that 0 examples do not suffice.
• PAC learnability of the thresholds θ ≤ 7 on ℕ via SOA and via optimalMistakeBound.
• optimalMistakeBound thresholdClass = ⊤: the theorem does not cover all thresholds, although VC theory does.

Manual impact

• Operator's Manual: new paragraph in "Online learning in the mistake-bound model" (topic order: after WINNOW1, before randomized learners), plus a cross-reference sentence in "Distribution-free realizable PAC learning".
• Agent Operator's Manual: no change needed. The PR adds no workflow, tooling or validation change.
• ROADMAP is left to the coordinator: this is a milestone, not the completion of the direction.

Validation

• lake build --wfail --iofail of the new module and test file: clean (no warnings).
• scripts/check_hygiene.py: passed.
• Full check: CI. The local quick check fell back to the full check because the manual changed.

Part of #4918.

AI disclosure: implemented by a Jetski AI agent as worker sgd under coordinator session 5f40c2da, for Samuel Schlesinger. Review is by agent review-c, which is agent review, not human review.

[SamuelSchlesinger]

Agent reviewer jrev-4932 (Jetski) is reviewing head f9d79f9 for coordinator jetski-coord-8077 (#4809). This is agent review, not human review.

[SamuelSchlesinger]

Reviewer review-c (Jetski swarm, coordinator session 5f40c2da; non-author agent review, not human review) at f9d79f9: APPROVE

What is proved. For a deterministic OnlineLearner A that is jointly measurable in (history, instance) for each history length, and D realizable by C:

• lintegral_error_prefixHypothesis_eq: 𝔼_{S∼D^m} error D (A after t examples) = D^{m+1}{A errs on example t}. This is the key step: Fin.removeNth t does not change the length-t prefix (prefixHypothesis_removeNth), so measurePreserving_piFinSuccAbove plus Measure.prod_apply_symm gives exactly this.
• sum_lintegral_error_prefixHypothesis_le: the sum over t ≤ m is the expected number of mistakes on m + 1 examples, at most M a.s. via IsRealizableBy.ae_realizable and mistakes_le_mistakeBound. This gives M/(m+1) for a uniformly random prefix hypothesis, the issue's bound in sum form.
• Majority vote: where prefixMajority errs, at least (m+1)/2 prefix hypotheses err (I checked both labels against the decide (m + 1 < 2 * #true) tie rule), so (m+1)·error ≤ 2·Σ error pointwise, then Markov gives IsPACLearnerFor m ε δ C (realizableDistributions C) when 2M ≤ εδ(m+1).
• Edge cases: M = 0 gives m = 0, and the bound reduces to error ≤ 0 for the empty-history hypothesis, which holds because a learner with mistake bound 0 is never wrong on any realizable point. not_isPACLearnerFor_three_zero shows that the 7-sample instance is not vacuous. The test optimalMistakeBound thresholdClass = ⊤ correctly marks where the theorem stops.

The model limits are stated accurately: the confidence dependence is 1/δ, not log(1/δ); the factor 2 comes from derandomization; IsMeasurableLearner is needed only off countable domains; no running time is claimed.

Source mapping (nit, non-blocking). The module docstring (lines 25–27), the sum_lintegral_error_prefixHypothesis_le docstring (245–249) and the manual call the random-prefix M/(m+1) statement "the online-to-batch conversion of [Littlestone1989] and [CesaBianchiConconiGentile2004]". As far as I know, Littlestone 1989's conversion is the hypothesis-testing scheme: keep the hypotheses, validate them on held-out data, get log(1/δ). The PR body correctly says that scheme is not formalized. The expectation identity "average risk of H_0..H_{n-1} has expectation 𝔼 M_n / n" is what CBCG 2004 (§II) uses. I suggest crediting the random-stopping expectation bound to CBCG 2004 and citing Littlestone 1989 as the origin of online-to-batch conversion and of the high-confidence version not formalized here. The locators are already labelled unverified, so this does not block.

Imports (nit). OnlineToBatch.lean:11: the public statements need only IsRealizableBy and realizableDistributions from PACLearning.Realizable. RealizableSample (ae_realizable) is used only in proofs, so public import ...PACLearning.Realizable plus plain import ...PACLearning.RealizableSample keeps the exported surface minimal.

Small proof duplication (nits).

• measurableSet_prefix_ne (131–136) restates measurableSet_misclassified (139–146) pulled back along S ↦ (S, S i). It could be a one-line preimage of the latter, which is the same move hF makes at line 202.
• isPACLearnerFor_prefixMajority re-derives hint (357–360), the last two steps of lintegral_error_prefixMajority_le's calc. A private lintegral_two_mul_sum_error_prefix_le (≤ 2 * M), used by both, would remove the repetition.

Reuse/placement. No parallel notion found. IsMeasurableLearner is new; the library has only hypothesis-level measurableSet_misclassified in RealizableSample, which this PR's private lemma of the same name does not shadow (it is private and namespaced). mistakes_eq_card, realizable_iff, mistakes_le_mistakeBound, ae_realizable and optimalError_eq_zero are reused. The placement under OnlineLearning/MistakeBound/ fits, since the module is about OnlineLearner/mistakeBound. @[expose] on the three definitions is justified: the decide tests unfold prefixHypothesis/prefixMajority, and clients off countable domains must unfold IsMeasurableLearner. Style is clean: simp only mid-proof, terminal simp_all <;> omega, header/marker/authors correct, bib entries in key order with correct venue/volume/pages/DOI.

Manuals. The Operator's Manual paragraph is in topic order (after WINNOW1, before randomized learners), names the API and the limits correctly, and links the module and tests. The cross-reference from the realizable-PAC section points to the right anchor. I agree that the Agent Operator's Manual needs no change (no workflow or tooling change). ROADMAP is left to the coordinator because this is a milestone of #4918; Part B remains.

CI. ci-checks, build and guide pass at f9d79f9. The Parallel-definition notice (3 definitions examined), the Duplicate-statement notice (18 theorems) and the Repeated-proof-block notice (18 proofs) are all empty, and my own source search agrees.

The nits above are optional follow-ups. Approving and queueing this head.

[SamuelSchlesinger]

Agent review (Jetski reviewer jrev-4932, coordinated by jetski-coord-8077 / #4809), head f9d79f9: APPROVE

The statements faithfully express the realizable online-to-batch conversion. lintegral_error_prefixHypothesis_eq uses measurePreserving_piFinSuccAbove to turn the expected error of the hypothesis after t examples into the probability of a mistake on a fresh example t. sum_lintegral_error_prefixHypothesis_le sums those probabilities to at most M, using IsRealizableBy.ae_realizable together with the existing mistakes_eq_card and mistakes_le_mistakeBound. The majority-vote derandomization (factor 2) and the Markov step then give the upstream deterministic IsPACLearnerFor m ε δ C (realizableDistributions C) for every realizable probability measure whenever 2M ≤ εδ(m+1). ⌈2M/(εδ)⌉₊ meets that bound.

The hypotheses are not vacuous. IsMeasurableLearner holds automatically on countable domains with measurable singletons. The tests show that 7 examples suffice and 0 do not for a three-concept class, and they cover the thresholds θ ≤ 7 both through SOA and through optimalMistakeBound.

I found no duplication with this repository, CSLib, Mathlib or #4933: the PR reuses the shared realizableDistributions and PAC definitions from main. The module is a small leaf with the correct upstream marker. The manual paragraph, its placement and the reason given for not editing the Agent Operator's Manual all check out, and the bibliography entries are sorted. ci-checks passes. Its parallel-definition, duplicate-statement and repeated-proof notices are empty. The only "PR description names" notice flags the two bibliography keys, which are not Lean declarations, so it is a false positive.

Non-blocking:

• At integration, add a comment to Online-to-batch conversion: SGD excess-risk bound and mistake bounds to PAC learning #4918 recording the bounded deliverable: IsMeasurableLearner on uncountable domains, 1/δ confidence rather than log(1/δ), and 2M/(m+1) for the deterministic learner versus the issue's M/(m+1), which is stated here only as the average over prefixes. Part B stays open.
• realizable_ofFn (OnlineToBatch.lean:238) is the general bridge from CSLib's sample Realizable to the list Realizable (useful to Sample compression schemes: the Littlestone–Warmuth bound and compression from mistake bounds #4914, for example). It could be public. Lines 404–407 rederive the iInf_lt_iff witness by contradiction.
• Optional: upstream IsRPACLearnerFor could carry the uniformly random prefix learner directly, with M ≤ εδ(m+1).

This is agent review, not human review.