[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 measureReal_empiricalFiniteMeasure_singleton_eq_pullCount and exp_mul_toReal_klDiv_empiricalFiniteMeasure (exp (card κ · KL(p̂ ‖ ν)) = ∏ᵢ p̂{x i} / ν{x i} for any finite family of points charged by ν). 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) and Nat.multinomial_mul_prod_pow_le_one (a multinomial probability is at most 1, in any ordered commutative semiring).
• LMLExplore/SequentialLearning/FiniteActions.lean: prod_pow_pullCount and prod_comp_pullCount, the multiplicative forms of LML's sum_pullCount_mul and 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. Tau Ceti's empiricalFiniteMeasure (with empiricalFiniteMeasure_apply and integral_empiricalFiniteMeasure_of_measurableSingletonClass) and Measure.rnDeriv_eq_measure_singleton_div give the divergence of the empirical distribution. The counts are LML's pullCount, not a new count, so the PR does not depend on the typeCount of #290. 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 built inline in the proof, following measure_exists_sum_div_add_sqrt_add_le_zero_le_of_iIndepFun (Probability/Martingale/SubGaussian.lean). 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