[RemyDegenne]

This PR proves the time-uniform concentration of the empirical distribution of independent observations on a finite type by the Laplace mixture [JKMDLV20, Proposition 1]. For ξ 0, ξ 1, … with law ν on a type with m elements, p̂_n the empirical distribution of the first n observations (Tau Ceti's empiricalFiniteMeasure) and δ > 0, it shows P(∃ n ≥ 1, log (1/δ) + (m - 1) log (e (1 + n / (m - 1))) ≤ n KL(p̂_n ‖ ν)) ≤ δ. It also proves that the likelihood ratio of every predictable sequential predictor against ν is a nonnegative supermartingale, and a mean-one martingale for a probability predictor when ν charges every point.

Target: ReinforcementLearning, Layer 3 "Concentration", item 4 "Types and categorical KL bounds", second bullet: "the likelihood ratio of every predictable sequential predictor against p is a nonnegative mean-one martingale. Laplace's predictor q_t(i) = (N_i(t)+1)/(t+m) gives, by Ville, P(∃ n ≥ 1, n KL(p̂_n, p) > log(1/δ) + (m-1) log(e(1+n/(m-1)))) ≤ δ". This PR proves that bullet. The event here uses ≤, so it contains the roadmap's event with >. The mean-one martingale statement needs ν to charge every point. Otherwise a predictor that puts mass on a ν-null point loses that mass, and only the supermartingale property holds, which is what Ville's inequality uses. The first bullet of item 4, the count of types and the (n+1)^m e^{-nε} bound, is the subject of the open PR #290. After this PR and #290, item 4 of Layer 3 is complete.

New declarations:

• LMLExplore/Probability/Martingale/LikelihoodRatio.lean: LMLExplore.predictorLikelihoodRatio ∏_{t<n} q t (ξ t) / ν{ξ t}, with _def, _zero, _succ and _nonneg; measurable_predictorLikelihoodRatio, integrable_predictorLikelihoodRatio, supermartingale_predictorLikelihoodRatio, martingale_predictorLikelihoodRatio and integral_predictorLikelihoodRatio (mean one). The observations are adapted to a filtration ℱ, with ξ t ℱ (t+1)-measurable, independent of ℱ t and of law ν. The predictor is ℱ t-measurable.
• LMLExplore/InformationTheory/LaplaceMixture.lean: LMLExplore.laplacePredictor (the rule of succession, with counts given by LML's pullCount), with _def, _nonneg, sum_laplacePredictor, measurable_laplacePredictor and the closed form prod_range_laplacePredictor ∏_{t<n} q_t(ξ t) = ∏ₐ N_n(a)! / m^{(n)}. It also has typeCount_eq_pullCount, identifying the type counts of ξ 0, …, ξ (n - 1) (typeCount of feat: the method of types and Sanov's bound on a finite type #290, InformationTheory/MethodOfTypes.lean) with LML's pullCount, so that the maximum-likelihood identity exp (n KL(p̂_n ‖ ν)) ∏_{t<n} ν{ξ t} = ∏ₐ (N_n(a)/n)^{N_n(a)} comes from MethodOfTypes' prod_measureReal_pow_typeCount_eq_mul_exp and measureReal_empiricalFiniteMeasure_singleton with toReal_klDiv_eq_sum_mul_log_div, and absolute continuity from empiricalFiniteMeasure_absolutelyContinuous. The comparison with the maximum likelihood is exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor. The time-uniform bound comes in two forms: measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le (filtration form) and ProbabilityTheory.iIndepFun.measure_exists_le_mul_klDiv_empiricalFiniteMeasure_le (independent form, reduced to the coordinates of ν^{⊗ℕ}).
• LMLExplore/Data/Nat/Choose/Bounds.lean: Nat.choose_le_exp_one_mul_div_pow (n.choose k ≤ (e n / k)^k), Nat.ascFactorial_div_factorial_le ((m+1)^{(n)} / n! ≤ (e (1 + n/m))^m), Nat.multinomial_mul_prod_pow_le_one (a multinomial probability is at most 1, in any ordered commutative semiring) and Nat.prod_div_pow_le_prod_factorial_div (∏ (f i / n)^{f i} ≤ ∏ (f i)! / n!, in any linearly ordered field).
• LMLExplore/Probability/Process/Filtration.lean: MeasureTheory.Filtration.naturalLT, the filtration of the strict past ⨆ j < i, comap (u j) of a measurable process, with naturalLT_apply, measurable_naturalLT (u j is measurable at every i > j) and indep_naturalLT (for independent u, u i is independent of naturalLT u hu i).
• LMLExplore/SequentialLearning/FiniteActions.lean: prod_comp_pullCount, the multiplicative form of LML's sum_comp_pullCount, and prod_range_pullCount_action_add_one ∏_{s<t} (N_s(A_s) + 1) = ∏ₐ N_t(a)!.

Proof of the threshold. Write N_n(a) for the count of a among the first n observations and P = ∏_{t<n} ν{ξ t}. The maximum likelihood is exp (n KL(p̂_n ‖ ν)) P = ∏ₐ (N_n(a)/n)^{N_n(a)}. The multinomial bound turns it into at most ∏ₐ N_n(a)! / n!. The rule of succession has likelihood L_n P = ∏ₐ N_n(a)! / m^{(n)}, and m^{(n)} / n! = binom(n+m-1, m-1) ≤ (e (1 + n/(m-1)))^{m-1}. Together these give exp (n KL) ≤ (e (1 + n/(m-1)))^{m-1} L_n. On the deviation event, L_n ≥ 1/δ, and LMLExplore's Ville inequality MeasureTheory.Supermartingale.measure_exists_le_le concludes.

Placement and reuse. The empirical distribution is Tau Ceti's empiricalFiniteMeasure, and its divergence is computed by the method-of-types identities of MethodOfTypes.lean (#290) through the bridge typeCount_eq_pullCount. The counts of the predictor are LML's pullCount, not a new count. SequentialLearning/LikelihoodRatio.lean handles mixtures of fixed alternatives along a bandit run, through exp (∑ log-likelihood ratios) integrated against a prior. A sequential predictor needs no prior, and the Laplace mixture would need the Dirichlet integral there, so the new file sits in Probability/Martingale/, next to Ville's inequality. The strict-past filtration of the coordinates of ν^{⊗ℕ} is Filtration.naturalLT; it lives in Probability/Process/Filtration.lean, which main had deleted after moving its only lemma, measurable_eval_piLE, to Statlib's measurable_piLE_apply (#350); the file now contains only naturalLT. It replaces the identical inline constructions in measure_exists_sum_div_add_sqrt_add_le_zero_le_of_iIndepFun (Probability/Martingale/SubGaussian.lean) and in the private exists_filtration_hasCondMGFBound (Probability/Martingale/RateFunction.lean), whose statements are unchanged. No public declaration is removed or renamed.

Source: the time-uniform bound is adapted from the paper project RemyDegenne/Essakine2026Tight at commit 38bbd16fd759008cf5dbad67b88e442df1d116fb (Apache 2.0), file Essakine2026Tight/ForLMLExplore/InformationTheory/KLTimeUniform.lean. That file proves the supermartingale property for the Laplace ratio only and bounds the mixture with Stirling's formula, which gives the threshold log (1/δ) + (m-1) log (n+1) + 1 + log n / 2. Following the note on R21 of its PAPER_ROADMAP.md, this port proves the property for every predictor and the roadmap's threshold of [JKMDLV20], through the multinomial bound. The source's Stirling helpers and its own threshold are not ported. The module docstring credits the source and the reference.

References: [JKMDLV20] A. Jonsson, E. Kaufmann, P. Ménard, O. D. Domingues, E. Leurent and M. Valko, Planning in Markov decision processes with gap-dependent sample complexity, NeurIPS 2020, Proposition 1. [EV26] Y. Essakine and C. Vernade, Tight sample complexity bounds for entropic best policy identification, Lemma 5.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R21

🤖 Prepared with Claude Code

[RemyDegenne]

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

The earlier duplication findings are fixed: the shared filtration, absolute continuity and the MethodOfTypes identities are now reused. The new public prod_pow_pullCount copies MethodOfTypes' prod_comp_eq_prod_pow_typeCount, and the PR's own bridge typeCount_eq_pullCount connects the two.

• LMLExplore/SequentialLearning/FiniteActions.lean:116 — prod_pow_pullCount (∏ a, f a ^ pullCount A a t ω = ∏ s ∈ range t, f (A s ω)) is a parallel API to prod_comp_eq_prod_pow_typeCount (∏ k, f (x k) = ∏ a, f a ^ typeCount x a) with the same prod_fiberwise' proof. Its only consumer, LaplaceMixture.lean:172, already has x and hN_type. Fix: Delete prod_pow_pullCount and its docstring entry. At LaplaceMixture.lean:172, rewrite P = ∏ t ∈ range n, ν.real {ξ t ω} as ∏ k, ν.real {x k} with Fin.prod_univ_eq_prod_range, then as ∏ a, ν.real {a} ^ typeCount x a with prod_comp_eq_prod_pow_typeCount (fun a ↦ ν.real {a}) x, so it matches h before hN_type is applied.

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 · 47s · 266.6k in (208.5k cache read, 58.1k cache write) / 3.8k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

Fixed in 6b4cd1b, following the first option of the finding.

• measureReal_empiricalFiniteMeasure_singleton_eq_pullCount_div is deleted. In its place is the bridge typeCount_eq_pullCount : typeCount (fun k : Fin n ↦ ξ k ω) a = pullCount ξ a n ω, proved from typeCount_def, card_filter, pullCount_eq_sum and Fin.sum_univ_eq_sum_range.
• h_max now comes from MethodOfTypes' prod_measureReal_pow_typeCount_eq_mul_exp hx, rewritten with measureReal_empiricalFiniteMeasure_singleton and the bridge, and from toReal_klDiv_eq_sum_mul_log_div (empiricalFiniteMeasure_absolutelyContinuous hx), as in measure_typeCount_eq_le. prod_pow_pullCount identifies ∏ₐ ν{a}^{N a} with ∏_{t<n} ν{ξ t}.
• exp_mul_toReal_klDiv_empiricalFiniteMeasure is deleted because it was the parallel proof of that identity and had no other use. The TauCeti...Decomposition.Lebesgue import it needed is dropped, and MethodOfTypes is now a public import because the bridge's statement uses typeCount.

Both deleted declarations were new in this PR, so no downstream use is affected. Local checks pass: the whole-library lake build --iofail succeeds, and local-axioms reports 0 violations across the 7 changed modules.

[RemyDegenne]

Re: your reply on reuse — re-reviewed on 6b4cd1b; the finding stands — The earlier duplication findings are fixed: the shared filtration, absolute continuity and the MethodOfTypes identities are now reused. The new public prod_pow_pullCount copies MethodOfTypes' prod_comp_eq_prod_pow_typeCount, and the PR's own bridge typeCount_eq_pullCount connects the two.

_{claude/claude-opus-5-5 · addresses your replies through comment 4569465490.}

[RemyDegenne]

Fixed in 375b19d, as the finding suggests.

• prod_pow_pullCount and its module-docstring entry are deleted from SequentialLearning/FiniteActions.lean. It was new in this PR, so nothing downstream used it.
• In exp_mul_toReal_klDiv_le_mul_predictorLikelihoodRatio_laplacePredictor (LaplaceMixture.lean), the left side ∏ a, ν.real {a} ^ typeCount x a of prod_measureReal_pow_typeCount_eq_mul_exp hx is rewritten with ← prod_comp_eq_prod_pow_typeCount (fun a ↦ ν.real {a}) x and then Fin.prod_univ_eq_prod_range, which gives P = ∏ t ∈ range n, ν.real {ξ t ω} before hN_type is applied.

This commit also merges current main (43d6b42); the merge had no conflicts. Local checks (not CI) pass: the whole-library lake build --iofail succeeds, and local-axioms reports 0 violations in the 7 changed modules.

[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.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
♻️	correctness	stale (re-run pending)	claude/claude-opus-5-5	Every new definition and statement (predictor likelihood ratio, its supermartingale/martingale properties, the Laplace closed form, the empirical KL identity, the comparison with the maximum likelihood and the time-uniform bound in both forms) matches the stated mathematics, including the m = 1 and δ ≥ 1 edge cases. The ≤ event contains the roadmap's strict event, and the extra hypothesis that ν charges every point is needed for the martingale claim.
🟡	reuse	changes requested	claude/claude-opus-5-5	The earlier duplication findings are fixed: the shared filtration, absolute continuity and the MethodOfTypes identities are now reused. The new public prod_pow_pullCount copies MethodOfTypes' prod_comp_eq_prod_pow_typeCount, and the PR's own bridge typeCount_eq_pullCount connects the two.
♻️	scope	stale (re-run pending)	claude/claude-opus-5-5	The PR proves the ReinforcementLearning Layer 3 item 4 second bullet (README.md:632-634) directly; the binomial/multinomial bounds, the pullCount product lemmas and the predictor likelihood-ratio supermartingale are all used directly in the final theorem, so it is one topic.
♻️	attribution	stale (re-run pending)	claude/claude-opus-5-5	Both new files name the Essakine2026Tight formalization at commit 38bbd16f and [JKMDLV20], and LaplaceMixture.lean also cites [EV26]. The remaining additions are routine or refactor existing in-repo constructions and need no further credit.
♻️	api-design	stale (re-run pending)	claude/claude-opus-5-5	The public surface is the predictor likelihood ratio, the rule of succession with its characterizing lemmas, the two Nat bounds and the time-uniform bound; the private helpers are specific to these proofs and no bodies are exposed. No compatibility layer is added and no duplicate of an existing declaration was found.
♻️	generality	stale (re-run pending)	claude/claude-opus-5-5	The statements are at the right level: the multinomial bound holds in any ordered commutative semiring, the supermartingale covers every sub-probability predictor, the pullCount products hold in any commutative monoid, and naturalLT replaces the two duplicated inline filtrations. The earlier finding about the twice-inlined absolute-continuity proof is fixed: both places now use empiricalFiniteMeasure_absolutelyContinuous from MethodOfTypes.lean.
♻️	placement	stale (re-run pending)	claude/claude-opus-5-5	Every new declaration sits in its natural home: the Laplace mixture is in InformationTheory/ next to the Krichevsky–Trofimov mixture, the predictor likelihood-ratio martingale is in Probability/Martingale/ next to Ville, the binomial and multinomial bounds mirror Mathlib's Data/Nat/Choose/Bounds, and the pullCount product lemmas sit beside their sum counterparts in FiniteActions.lean. None of the imports is unused or overly broad.
♻️	naming	stale (re-run pending)	claude/claude-opus-5-5	The earlier _eq_pullCount overstatement is fixed by the rename to measureReal_empiricalFiniteMeasure_singleton_eq_pullCount_div, which matches the repo's pullCount_div usage. The other new names describe their conclusions, follow the existing iIndepFun. and Filtration.natural patterns, and the PR adds no notation.
♻️	documentation	stale (re-run pending)	claude/claude-opus-5-5	All new files have accurate module docstrings, and every public definition and main theorem has a docstring that matches its statement, with no roadmap or process narrative. Checked claims (the ascending factorial convention, the m = 1 remark, the ≤-versus-> remark, the cross-reference to SequentialLearning/LikelihoodRatio.lean) are correct.
♻️	proof-quality	stale (re-run pending)	claude/claude-opus-5-5	All three earlier findings are fixed: the absolute-continuity step uses the shared empiricalFiniteMeasure_absolutelyContinuous, the strict-past filtration is the reusable Filtration.naturalLT used at all three call sites, and the multinomial and binomial bounds are standalone lemmas in Bounds.lean. The remaining long proof, setIntegral_predictorLikelihoodRatio_succ, is broken into commented steps, and no proof relies on undocumented definitional equality.

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

_{Reviewing this diff at head 6b4cd1b. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.24.}

[lmlexplore-automation]

⚠️ This PR no longer merges into main. Rebase it onto current main (or merge main into it) and push — nothing downstream can make progress until then, since a green build and an approving review on this head still cannot merge.

Do check what the conflict actually is before resolving it mechanically. If main has since landed its own version of something this PR adds, part of it may be superseded, and the right answer is to drop that part — or close the PR — rather than to reconcile the text. That is an authoring decision.