[RemyDegenne]

This PR adds the method of types on a finite type and Sanov's deviation bound for the empirical distribution of an i.i.d. sample. It is the first bullet of ReinforcementLearning Layer 3.4 ("Types and categorical KL bounds"): on a set of size m, there are at most (n+1)^m types, and P(KL(p̂ₙ, p) > ε) ≤ (n+1)^m e^{-nε}. Both are proved here with the sharper exponent m - 1, which implies the roadmap's m, and for any m, not only m ≥ 2. Layer 19 (best policy identification, through the confidence threshold of RF-Express and of entropic BPI) lists Layer 3.4 as a prerequisite. After this PR, the rest of Layer 3.4 is its second bullet: the martingale property of the likelihood ratio of predictable predictors, and the time-uniform bound for Laplace's predictor.

LMLExplore/InformationTheory/MethodOfTypes.lean (new) contains:

• LMLExplore.typeCount (the type a ↦ #{k | x k = a} of x : Fin n → α, body not exposed) with typeCount_def, typeCount_pos_iff, typeCount_eq_zero_iff, sum_typeCount, typeCount_mem_piAntidiag and prod_comp_eq_prod_pow_typeCount;
• card_image_typeCount_le, the number of types: at most (n + 1) ^ (m - 1) [CT, Theorem 11.1.1];
• measureReal_empiricalFiniteMeasure_singleton, which says Tau Ceti's empirical measure gives a the mass typeCount x a / n, and empiricalFiniteMeasure_absolutelyContinuous;
• pi_setOf_typeCount_eq, the product measure of a type class;
• prod_measureReal_pow_typeCount_eq_mul_exp, the ratio exp (-n KL) of the probabilities of a sequence under ν and under its empirical distribution [CT, Theorem 11.1.2];
• measure_typeCount_eq_le, the probability of a type class, at most exp (-n t) for t ≤ KL(p̂(x) ‖ ν) [CT, Theorem 11.1.4];
• measure_lt_klDiv_empiricalFiniteMeasure_le, Sanov's bound ℙ(KL(p̂ₙ ‖ ν) > t) ≤ (n + 1) ^ (m - 1) exp (-n t) [CT, Theorem 11.2.1], [EV26, Lemma 19], and its confidence form measure_log_div_lt_klDiv_empiricalFiniteMeasure_le.

The empirical distribution is Tau Ceti's TauCeti.Probability.empiricalFiniteMeasure, not a new definition. The law ν is any measure on a finite type with measurable singletons; it is a probability measure by the HasLaw hypotheses. The law of the sample is Mathlib's iIndepFun.hasLaw_pi.

There are two supporting additions. LMLExplore/Algebra/Order/Antidiag/FinsuppEquiv.lean (new) has Finset.card_piAntidiag_nat_eq_choose, which is stars and bars for Finset.piAntidiag, proved from Mathlib's card_finsuppAntidiag_nat_eq_choose, and Finset.card_piAntidiag_nat_le_pow, the bound (n + 1) ^ (#s - 1), proved from Mathlib's Nat.choose_add_le_add_one_pow. LMLExplore/InformationTheory/KullbackLeibler/Finite.lean gains LMLExplore.toReal_klDiv_eq_sum_mul_log_div: for finite measures μ ≪ ν on a finite type, (klDiv μ ν).toReal = ∑ a, μ{a} log (μ{a}/ν{a}) + ν(univ) - μ(univ). This is the bridge that file's docstring already describes between measure KL and vector relative entropy. Unlike Tau Ceti's TauCeti.klDiv_eq_ofReal_sum_log_singleton, it allows atoms of ν with mass zero. Its proof evaluates the Radon–Nikodym derivative at atoms with Tau Ceti's Measure.rnDeriv_eq_measure_singleton_div.

No public declaration is removed or renamed.

Source: this ports item R20 of the paper project RemyDegenne/Essakine2026Tight (commit 520dd39a55fa4e9a62a4a2d51f48163926176a5d, Apache 2.0 license), files ForLMLExplore/InformationTheory/MethodOfTypes.lean and ForLMLExplore/InformationTheory/KullbackLeibler/Fintype.lean. It was adapted as follows:

• the statements are on a general law ν and Tau Ceti's empirical measure, instead of weightedMeasure p and a local empiricalFreq;
• the counting of types goes through Mathlib's stars and bars instead of an ad hoc injection;
• the KL formula is generalised to finite measures and placed in KullbackLeibler/Finite.lean;
• the wrapper klDiv_ne_top_of_finite is inlined as Mathlib's klDiv_ne_top;
• the citations are kept: [CT] Cover–Thomas, Elements of Information Theory, and [EV26] Essakine–Vernade, COLT 2026, arXiv:2605.13717. The exponent m - 1 corrects the m in the proof of [EV26, Lemma 19] (the paper's errata E22).

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R20

🤖 Prepared with Claude Code

[RemyDegenne]

🟡 attribution — request_changes claude/claude-opus-5-5

The informal sources [CT] and [EV26] are cited, but neither ported file credits the formalization in RemyDegenne/Essakine2026Tight that the description says it ports from.

• LMLExplore/InformationTheory/MethodOfTypes.lean:42 — The module docstring does not credit the formalization this file is adapted from (Essakine2026Tight, ForLMLExplore/InformationTheory/MethodOfTypes.lean, commit 520dd39a, Apache 2.0). That source is named only in the PR description. Fix: Add a sentence before ## References, e.g. "The method-of-types bounds are adapted from ForLMLExplore/InformationTheory/MethodOfTypes.lean of the formalization Essakine2026Tight (github.com/RemyDegenne/Essakine2026Tight, by Rémy Degenne, Apache 2.0) of [EV26]."
• LMLExplore/InformationTheory/KullbackLeibler/Finite.lean:209 — toReal_klDiv_eq_sum_mul_log_div is described in the PR as a generalisation of Essakine2026Tight's ForLMLExplore/InformationTheory/KullbackLeibler/Fintype.lean, but neither the docstring nor the module doc credits that source. Fix: Add a line to the module docstring saying that toReal_klDiv_eq_sum_mul_log_div is adapted (generalised to finite measures) from ForLMLExplore/InformationTheory/KullbackLeibler/Fintype.lean of the formalization Essakine2026Tight.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 28s · 108.3k in (98.2k cache read, 10.1k cache write) / 1.9k out tokens · reviewing this diff · rubric}

[RemyDegenne]

🟡 api-design — request_changes claude/claude-opus-5-5

The surface is minimal and typeCount's body is hidden behind typeCount_def := (rfl), but the empirical-mass evaluation lemma has no @[simp] and typeCount lacks its positivity/zero characterization.

• LMLExplore/InformationTheory/MethodOfTypes.lean:108 — measureReal_empiricalFiniteMeasure_singleton is the normal form for the mass of a singleton under the empirical measure but has no @[simp], unlike the parallel measureReal_empiricalKernel_apply_singleton. Fix: Tag it @[simp].
• LMLExplore/InformationTheory/MethodOfTypes.lean:62 — typeCount has no lemma characterizing when a count is positive or zero. The proof of measure_typeCount_eq_le gets positivity from card_pos.2 ⟨k, by simp⟩ (line 164), which relies on unfolding the definition in its own file; users elsewhere would have to rewrite with typeCount_def. Fix: Add typeCount_pos_iff : 0 < typeCount x a ↔ ∃ k, x k = a and @[simp] typeCount_eq_zero_iff : typeCount x a = 0 ↔ ∀ k, x k ≠ a, and use them at line 164.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 32s · 106.1k in (95.7k cache read, 10.4k cache write) / 2.7k out tokens · reviewing this diff · rubric}

[RemyDegenne]

Addressed in 6876351, with one part contested.

Fixed: typeCount positivity and zero. I added typeCount_pos_iff : 0 < typeCount x a ↔ ∃ k, x k = a and @[simp] typeCount_eq_zero_iff : typeCount x a = 0 ↔ ∀ k, x k ≠ a. The proof of measure_typeCount_eq_le (and the new prod_measureReal_pow_typeCount_eq_mul_exp) now uses typeCount_pos_iff instead of card_pos.2 ⟨k, by simp⟩. simpNF accepts typeCount_eq_zero_iff.

Contested: @[simp] on measureReal_empiricalFiniteMeasure_singleton. I tried the tag, and the environment linter rejects it. Tau Ceti's TauCeti.Probability.empiricalFiniteMeasure_toMeasure is already @[simp] and rewrites the coercion (empiricalFiniteMeasure x : Measure α) inside the left-hand side, so simp never reaches this lemma:

simpNF LMLExplore.measureReal_empiricalFiniteMeasure_singleton: Left-hand side simplifies from
  (↑(TauCeti.Probability.empiricalFiniteMeasure x)).real {a}
to
  (∑ x_1, (↑n)⁻¹ • MeasureTheory.Measure.dirac (x x_1)).real {a}
using
  simp only [*, @TauCeti.Probability.empiricalFiniteMeasure_toMeasure, Fintype.card_fin]
Try to change the left-hand side to the simplified term!

The parallel measureReal_empiricalKernel_apply_singleton can be @[simp] because nothing unfolds empiricalKernel N ω a first. Here, adding the tag would break CI (linters run with warnings as errors), and silencing the linter is not allowed. So the lemma stays untagged and is used by name with rw.

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

Sanov's bound ends a cast step with an undocumented rfl, and the reusable ratio identity is buried in a ~60-line proof. Several long named-lemma rewrite chains are brittle.

• LMLExplore/InformationTheory/MethodOfTypes.lean:229 — After push_cast in measure_lt_klDiv_empiricalFiniteMeasure_le, a bare rfl closes the goal. This relies on an undocumented definitional equality between cast forms in ℝ≥0∞/ℝ. Fix: Replace push_cast; rfl with simp/norm_cast or an explicit cast lemma, or add a comment saying which defeq rfl uses.
• LMLExplore/InformationTheory/MethodOfTypes.lean:176 — hkey (with its helper hexp) proves ∏ ν{a}^N a = (∏ Q{a}^N a) · exp(-n·∑ Q log(Q/ν)), the reusable identity [CT, Theorem 11.1.2]. It sits inline in measure_typeCount_eq_le, which runs about 60 lines (138–199). Fix: Make it a standalone lemma (e.g. prod_measureReal_pow_typeCount_eq_mul_exp) about x and ν with the support hypothesis, and call it from measure_typeCount_eq_le.
• LMLExplore/InformationTheory/MethodOfTypes.lean:185 — hexp is closed by a 9-lemma rw chain (← mul_assoc, hQ a, mul_div_cancel₀, ← hQ a, ← mul_neg, ← log_inv, inv_div, ← log_pow, exp_log) that is fragile under Mathlib renames. The same pattern appears in hQle (lines 164–165, a 6-rewrite rwa) and in measure_log_div_lt_klDiv_empiricalFiniteMeasure_le (lines 243–244, 8 rewrites). Fix: Prove hexp as exp(-(N a * log (Q/ν))) = (ν/Q)^N a via Real.exp_log/rpow_natCast plus field_simp/simp. Shorten the other two chains with simp [ENNReal.toReal_prod, ...] and Real.exp_log followed by field_simp.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 44s · 47.8k in (41.5k cache read, 6.3k cache write) / 3.1k out tokens · reviewing this diff · rubric}

[RemyDegenne]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The type-count bound, the type-class probability bound, Sanov's bound (with the sharper exponent m-1) and its confidence form match the roadmap's Layer 3.4 first bullet and the CT statements, and the edge cases (ν-null atoms, KL = ⊤, n = 0, empty index set, negative t) are handled soundly. The finite-type KL formula correctly includes Mathlib's mass correction term and handles atoms of ν with mass zero.
✅	reuse	approved	claude/claude-opus-5-5	The new material (type counting, stars-and-bars bound for piAntidiag, finite-type KL formula, Sanov's bound) is not in Mathlib or LMLExplore, and it reuses card_finsuppAntidiag_nat_eq_choose, Nat.choose_add_le_add_one_pow, prod_fiberwise', toReal_klDiv, integral_fintype and iIndepFun.hasLaw_pi instead of re-deriving them. TauCeti sources were not in the checkout, so the empirical-measure lemmas were not checked against it.
✅	scope	approved	claude/claude-opus-5-5	The PR directly proves the first bullet of ReinforcementLearning Layer 3.4 (at most (n+1)^m types and Sanov's KL deviation bound), with a sharper exponent. The stars-and-bars count and the finite-type KL formula are direct prerequisites used in the main proofs, so the PR is a single coherent topic.
🟡	attribution	changes requested	claude/claude-opus-5-5	The informal sources [CT] and [EV26] are cited, but neither ported file credits the formalization in RemyDegenne/Essakine2026Tight that the description says it ports from.
🟡	api-design	changes requested	claude/claude-opus-5-5	The surface is minimal and typeCount's body is hidden behind typeCount_def := (rfl), but the empirical-mass evaluation lemma has no @[simp] and typeCount lacks its positivity/zero characterization.
✅	generality	approved	claude/claude-opus-5-5	The statements are at the natural level: stars-and-bars is stated for general Finset.piAntidiag, the KL bridge for finite measures with μ ≪ ν, and the Sanov bounds for an arbitrary law ν on a finite type, with no unused or too-strong hypotheses. I found no special-case duplication or speculative abstraction.
✅	placement	approved	claude/claude-opus-5-5	New material sits in fitting homes: the stars-and-bars count mirrors Mathlib's Antidiag/FinsuppEquiv path, the measure-to-vector KL bridge is in KullbackLeibler/Finite.lean as its docstring anticipates, and the method of types gets its own InformationTheory file. All added imports are used and specific.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology, the strength of each name matches its statement (_le for inequalities, _eq for equalities), and the namespaces fit; the Finset counting lemmas sit beside Mathlib's card_finsuppAntidiag_nat_eq_choose. The PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	Each new file opens with a module docstring that says what it contains and what it feeds, and every new public definition and main theorem has a docstring that matches its statement, with no overclaims and no process narrative. The citations to Cover–Thomas Theorems 11.1.1, 11.1.4 and 11.2.1 match the results proved.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	Sanov's bound ends a cast step with an undocumented rfl, and the reusable ratio identity is buried in a ~60-line proof. Several long named-lemma rewrite chains are brittle.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 47624e6. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.34.}