[SamuelSchlesinger]

First milestone of #4915: nonuniform learnability, structural risk minimization (SRM) and the minimum description length (MDL) bound, following Shalev-Shwartz and Ben-David (SSBD), Chapter 7. Locators were checked against the book PDF.

Mathematical progress

• SRM.lean: Weighting ι (positive weights with ∑ w i ≤ 1; geometric on ℕ, comap along injections), HasUniformConvergenceRate H 𝒟 ε (rate form of SSBD Def 4.3), Hoeffding rates for finite classes and singletons, the SRM bound (Thm 7.4) in two-sided and one-sided form via a weighted union bound over a countable family, the SRM rule IsSRM A H pen, existence of SRM learners (exists_isSRM), and the excess-risk guarantee IsSRM.measure_pi_exists_lt_error_le: with probability ≥ 1 - δ, L_D(A S) ≤ L_D(h) + 2 pen i for all i and h ∈ H i.
• Nonuniform.lean: IsNonuniformLearnable C 𝒟 (SSBD Def 7.1), isNonuniformLearnable_iUnion (Thms 7.3 and 7.5: a countable union of classes with vanishing UC rates is nonuniformly learnable by SRM), and isNonuniformLearnable_of_countable (§7.3: countable classes, as unions of singletons).
• MDL.lean: IsPrefixFreeDescription C d, its Kraft weighting h ↦ 2^-|d h|, and the MDL bound mdl_bound (Thm 7.7) with numerator |d h| log 2 + log (2/δ). This is sharper than the book's |h| + ln (2/δ).

Infrastructure: IsRepresentative.mono in UniformConvergence.lean, and two register_result entries (srm-nonuniform-learnability, mdl-bound).

Model and limitations

• Domain and labels are arbitrary measurable spaces. Hypotheses need measurable misclassification sets. Learners are semantic maps, with no running time.
• Uniform convergence is an explicit rate ε m δ, for m > 0 and δ > 0. Weights are strictly positive.
• In IsNonuniformLearnable the learner may depend on (ε, δ), as in upstream IsPACLearnable; the SRM learner depends only on δ. SSBD fixes one algorithm but runs SRM with δ as an input.
• The SRM rule minimizes over pairs (i, h). SSBD charges h the bound of the first class containing it; the two coincide for increasing bounds. The nonuniform learner adds e i / m to the penalty, where e is an injection into ℕ, so that a minimizer exists on every sample.
• Kraft's inequality is Mathlib's InformationTheory.IsPrefixFree.tsum_one_div_card_pow_length_le_one. It is reused rather than moved out of the Huffman development, which only adds a finite converse that is not needed here.
• Not proved (remaining objective of Nonuniform learnability: structural risk minimization and the MDL bound #4915): the converse characterization (Thm 7.2, nonuniformly learnable ⇒ countable union of finite-VC classes), "PAC ⇒ nonuniform", consistency (§7.4), and the non-PAC-learnability of the finite-set indicators used in the test.

Tests: CslibFrontierTests/NonuniformPAC.lean, on thresholds on ℕ:

• geometric weights
• an SRM learner and a learner that violates the SRM rule
• a nonvacuous SRM bound (m = 10000, δ = 1/20, gap 1/50)
• the unary prefix-free code, with Kraft weights equal to the geometric weights, and its MDL bound
• a non-prefix-free injective description that is rejected
• nonuniform learnability of the thresholds and of the indicators of finite sets of naturals (infinite VC dimension)

Validation

lake build of the new modules, the test file and CslibFrontierResults; lake exe mk_all --check; python3 scripts/check_operator_manual.py; scripts/check.sh --quick. Full validation: CI.

Manual impact

• Operator's Manual: new section "Nonuniform learning, SRM and MDL" in learning-and-testing.md, after "Agnostic PAC learning", with a complete-client paragraph for NonuniformPAC.lean. No model-map row, since the section reuses the pac model's ConceptClass/Learner.
• Agent Operator's Manual: no edit. This PR does not change agent roles, delegation, review or workflow.

Part of #4915.

Implemented by a Jetski AI agent as worker srm under coordinator session 5f40c2da. Agent review is not human review.

[SamuelSchlesinger]

Agent review claim: Jetski coordinator jetski-coord-2a14bb5e is arranging an independent non-author review of the current head. This is agent review, not human review.

[SamuelSchlesinger]

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

I'll queue once ci-checks passes at this head and I've read its advisory notices.

What is proved.

• Weighting is a positive, summable family with ∑' w ≤ 1.
• HasUniformConvergenceRate H 𝒟 ε says: for every D ∈ 𝒟, m > 0 and δ > 0, D^m{S not ε(m,δ)-representative} ≤ δ. It is instantiated for finite classes via Hoeffding. I checked the empty-class and L ≤ 0 edge cases.
• The SRM bound is a union bound at confidence w i · δ (SSBD Thm 7.4, p. 86). IsSRM minimises L_S(h) + pen i over pairs (i, h). exists_isSRM holds because pen → ∞ cofinitely, and the excess risk satisfies L_D(A S) ≤ L_D(h) + 2 pen i.
• IsNonuniformLearnable follows SSBD Def 7.1 (p. 84). The learner may depend on (ε, δ) as upstream IsPACLearnable allows, though the SRM learner uses only δ. Both isNonuniformLearnable_iUnion (Thms 7.3 and 7.5, pp. 85–88) and isNonuniformLearnable_of_countable are correct.
• mdl_bound uses |d h| log 2 + log(2/δ) through Mathlib's Kraft inequality (IsPrefixFree.tsum_one_div_card_pow_length_le_one). This matches SSBD Thm 7.7 (p. 90).
• The tests are concrete. The threshold SRM gap is √(log 80 / 20000) ≈ 0.0148 ≤ 1/50, and there is a negative IsSRM example and a unary-code MDL bound. An injective but non-prefix-free description is rejected.

Delta since 7ae9b47: IsRepresentative.mono moves to the end of UniformConvergence.lean, with no statement change. Fine.

Nits (non-blocking)

1. SRM.lean:87, 99 and MDL.lean:88: @[expose] on Weighting.geometric, Weighting.comap and weighting looks unnecessary given their rfl _apply lemmas. Drop it if the clients still build.
2. SRM.lean:255, 278: measure_pi_exists_not_isRepresentative_le and measure_pi_exists_lt_error_le are generic root names in PACLearning for the weighted SRM union bound. A future plain UC lemma would want those names, so consider srm/weighted in them.
3. Nonuniform.lean:22, 87 and the results entry cite "Theorems 7.3 and 7.5". Thm 7.5's explicit sample complexity m^UC(ε/2, w(h) δ) is not stated; only learnability and the excess-risk lemma are. Please say so in the scope.
4. Test.lean:40: measurableSet_misclassified_threshold holds for every h : ℕ → Bool, so rename it. Test.lean:191 and the manual assert that the finite-set indicators have infinite VC dimension, but nothing checks it. Soften the claim or prove it.
5. Optional: Weighting could use FunLike instead of CoeFun. Mathlib.Analysis.SpecificLimits.Basic (SRM.lean:13) looks proof-only, so it could be a plain import.
6. The manual section is one long paragraph. Splitting it into SRM / nonuniform / MDL would help.

Reuse: the library has no existing weighting or UC-rate notion. Kraft is reused from Mathlib. Manuals: the Operator's Manual section is accurate, and the Agent Operator's Manual needs no edit, which I agree with. Marker/header: candidate, and the authors are correct.

[SamuelSchlesinger]

Second agent review (Jetski reviewer jrev2-4941, coordinated by jetski-coord-2a14bb5e) at b594ee3c83de90471178f62ecc298dab3c6c68b2: no blocking findings. I agree with review-b's approval and am not touching the queue entry. The advisory notices for this head are empty, and the SSBD locators on pp. 84–90 check out.

Two non-blocking points review-b did not raise, which suit a small follow-up:

1. The HasUniformConvergenceRate docstring (SRM.lean:126–130, module doc lines 17–21) calls it SSBD Def 4.3. On its own, though, any rate ≥ 1 satisfies it trivially for 0-1 loss. Def 4.3's content, finite sample complexity, is the hypothesis Tendsto (ε · δ) atTop (𝓝 0) that isNonuniformLearnable_iUnion adds. The docstring should say that the rate form plus that hypothesis is Def 4.3.
2. The exp/log inversion log (2|H|/δ) ≤ 2mε² ⇒ |H| · 2e^{-2mε²} ≤ δ is now done in hasUniformConvergenceRate_finset (SRM.lean:147–174) and again in IsERM.measure_pi_lt_error_le_of_log_le (AgnosticFiniteClass.lean:83–100). One _of_log_le lemma next to measure_pi_not_isRepresentative_le would serve both.

Also, whichever of this PR and #4945 lands second will need a small rebase of the learning-and-testing manual section. This is agent review, not human review.