[RemyDegenne]

This PR proves the bounded instance of conditional MGF domination asked for in the Bandits roadmap, Layer 1.4 (Chernoff bounds in rate-function form): "a random variable with values in $[0,1]$ whose conditional mean given a σ-algebra is at most (at least) $m$ is conditionally dominated by $\mathcal B(m)$ on $[0,\infty)$ (on $(-\infty,0]$) [GC11, Lemma 9; LS, Note 10.3.1]". It then feeds the result into the existing filtration-level self-normalized deviations (Probability/Martingale/RateFunction.lean). That gives [GC11, Theorem 10] for $[0,1]$-valued rewards with bounded conditional means and adapted selection indicators, without independence.

Roadmap: Bandits

The new file is LMLExplore/Probability/Martingale/KLChernoff.lean (288 lines, namespace LMLExplore). It is the conditional companion of Probability/Moments/KLChernoff.lean, just as Martingale/RateFunction.lean is to Moments/RateFunction.lean.

Main declarations:

• hasCondMGFBound_Ici_cgf_bernoulliMeasure, hasCondMGFBound_Iic_cgf_bernoulliMeasure: for a measurable X ∈ [0, 1] a.s. with μ[X | m] ≤ q (resp. q ≤ μ[X | m]) a.s., HasCondMGFBound m hm X (cgf id Ber((1 : ℝ), 0, q)) (Set.Ici 0) μ (resp. Set.Iic 0). The proof applies the existing unconditional mgfDominatedOn_Ici_bernoulliMeasure / mgfDominatedOn_Iic_bernoulliMeasure to the conditional expectation kernel at almost every point.
• measure_exists_gt_and_le_mul_klBer_le_of_condExp_le, measure_exists_lt_and_le_mul_klBer_le_of_le_condExp: for X k ∈ [0, 1] that are ℱ (k + 1)-measurable with E[X k | ℱ k] ≤ m (resp. ≥ m), and adapted selection indicators w k ∈ {0, 1}: P(∃ t, 1 ≤ N t ≤ n, m < μ̂ t, x ≤ N t d(μ̂ t, m)) ≤ e ⌈x log n⌉ exp (-x), and the same below m. These consume the two domination theorems through measure_exists_gt_and_le_mul_rateFunction_le / measure_exists_lt_and_le_mul_rateFunction_le and rateFunction_id_bernoulliMeasure.
• measure_exists_klUpper_lt_le_of_le_condExp, measure_exists_lt_klLower_le_of_condExp_le: the time-uniform coverage of the KL-UCB upper and lower confidence levels U(μ̂ t, x / N t) and L(μ̂ t, x / N t) along a filtration.

General supporting lemmas (public, in their canonical homes; added after review):

• LMLExplore.hasCondMGFBound_cgf_of_ae_mgfDominatedOn (Probability/Moments/MGF/Bound.lean): if exp (t X) is integrable and, under almost every conditional law condExpKernel μ m ω', X is dominated by Y under Q on Λ (MGFDominatedOn), then HasCondMGFBound m hm X (cgf Y Q) (Λ ∩ integrableExpSet Y Q) μ. This is the conditional analogue of mgfDominatedOn_iff_hasMGFBound, and both Bernoulli dominations are derived from it.
• LMLExplore.ae_trim_ae_condExpKernel (Probability/Kernel/Condexp.lean): a μ-a.e. property holds a.e. under condExpKernel μ m ω for μ.trim hm-a.e. ω. The kernel-mean identity is Mathlib's condExp_ae_eq_trim_integral_condExpKernel.
• LMLExplore.le_of_ae_le_of_condExp_le, LMLExplore.le_of_le_condExp_of_ae_le (new MeasureTheory/Function/ConditionalExpectation/Real.lean): under a nonzero finite measure, a ≤ f a.e. and μ[f | m] ≤ c a.e. give a ≤ c; c ≤ μ[f | m] a.e. and f ≤ b a.e. give c ≤ b.
• The weighted mean of [0, 1]-valued rewards lying in [0, 1] uses Mathlib's Convex.centerMass_mem instead of a local lemma.

Consumers and dependency edge: the roadmap's Layer 1.4 names this instance as the bounded case of the Identification roadmap's Layer 4.2 conditional domination (HasCondMGFBound, its exponential supermartingales and the self-normalized deviations [GC11, Theorem 10], all already on main). The Identification README's Layer 4.2 bullet on exponential-family cumulant generating functions likewise says "the domination of $[0,1]$-valued variables by Bernoulli laws is the Bandits roadmap's Layer 1.4". The existing iIndepFun bounds in Moments/KLChernoff.lean are the independent, every-variable-selected case.

What remains of Layer 1.4 after this PR: nothing in its statement. The i.i.d. consequences [LS, Lemma 10.3, Corollary 10.4] were already merged in Moments/KLChernoff.lean. The only gap is that the upper-tail bound measureReal_sum_ge_le_exp_klBerReal still assumes a mean m > 0.

No declarations are removed or renamed, and no Mathlib material is vendored. Sources are credited in the module docstring: Garivier and Cappé, The KL-UCB algorithm for bounded stochastic bandits and beyond (COLT 2011), Lemma 9 and Theorem 10; Lattimore and Szepesvári, Bandit Algorithms, Note 10.3.1.

Reuse checks: I grepped Mathlib, Tau Ceti, LML and LMLExplore/ for conditional Bernoulli or [0, 1] MGF bounds. Every existing HasCondMGFBound instance is Gaussian, sub-exponential or comes from independence. The only Bernoulli dominations are the unconditional mgfDominatedOn_I{ci,ic}_bernoulliMeasure, which this PR reuses. SequentialLearning/BernoulliDeviation.lean is a different argument: a Krichevsky–Trofimov mixture for Bernoulli bandits.

Local checks (not CI): tauceti-local-checks verify --policy ordinary passed, with scope: scoped: against dca76852a43d553a35fb2afa9d31ae4b37501dde and local-axioms: checked 4 changed module(s), 76 declaration(s); 0 violation(s). The full lake build passed, along with the module-system, header-style and environment-lint checks.

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — approved

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	approved	claude/claude-opus-5-5	The conditional Bernoulli domination theorems and the filtration-level GC11 Theorem 10 and KL-UCB coverage consequences state the intended results with correct quantifiers, measurability, conditioning and tail directions, and m outside [0,1] is handled by proof rather than by hypothesis. The supporting lemmas (ae_trim_ae_condExpKernel, hasCondMGFBound_cgf_of_ae_mgfDominatedOn, the constant condExp bounds) are faithful, and they add no new predicates.
✅	reuse	approved	claude/claude-opus-5-5	The conditional Bernoulli dominations, the general kernel-domination bridge and the filtration-level KL bounds are new, and they reuse the existing unconditional Bernoulli dominations, rate-function deviations and rateFunction_id_bernoulliMeasure. Mathlib has no general version of ae_trim_ae_condExpKernel (only the fixed-property aestronglyMeasurable_trim_condExpKernel), and the private helpers are short plumbing with no located replacement.
✅	scope	approved	claude/claude-opus-5-5	The conditional Bernoulli domination is the exact statement of the Bandits roadmap's Layer 1.4 (README.md:269-271), and the general helper lemmas are direct prerequisites used by its proofs. The GC11 Theorem 10 corollaries along a filtration apply that result through the existing RateFunction bounds, so the PR is a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The new module and theorem docstrings credit the informal sources followed (GC11 Lemma 9 and Theorem 10; LS Note 10.3.1) and name the in-repo declarations the proofs build on; the supporting lemmas are routine Mathlib compositions needing no external credit. The roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The prior findings are resolved: the general condExp bounds, the condExpKernel a.e. transfer and the conditional domination lemma are now public in their canonical homes, and the weighted-mean helper is replaced by Mathlib's Convex.centerMass_mem. The remaining private helpers depend on this file's {0,1} weights or Bernoulli/KL setting, or are trivial one-off rewrites, and the six theorems in Martingale/KLChernoff.lean are the right Layer 1.4 surface.
✅	generality	approved	claude/claude-opus-5-5	The conditional Bernoulli dominations are derived from a general kernel-level domination lemma (hasCondMGFBound_cgf_of_ae_mgfDominatedOn), and the filtration theorems take the same hypotheses as the upstream RateFunction results they specialize. There are no unused or overly strong assumptions, no special-case duplication, and no speculative parameters.
✅	placement	approved	claude/claude-opus-5-5	The new conditional KL-Chernoff file sits in Probability/Martingale/ as the companion of Moments/KLChernoff.lean, and each general supporting lemma lives in its canonical home (MGF/Bound.lean, Kernel/Condexp.lean, ConditionalExpectation/Real.lean). Imports are specific and none is evidently unused.
✅	naming	approved	claude/claude-opus-5-5	The new names reuse the adjacent unconditional names (measure_exists_*_klBer_le, measure_exists_kl{Upper,Lower}_*, mgfDominatedOn_I{ci,ic}_bernoulliMeasure) and the hasCondMGFBound_cgf_* precedent, with correct _of_condExp_le/_of_le_condExp hypothesis suffixes. No notation is introduced and none of the names claims more than its statement proves.
✅	documentation	approved	claude/claude-opus-5-5	The new files have accurate module docstrings with the GC11 and LS references and no roadmap or process narrative. All new public declarations, including the supporting lemmas in Bound.lean, Condexp.lean and Real.lean, have docstrings that match their hypotheses and conclusions, and the cross-reference to the independent bounds in Moments/KLChernoff is correct.
✅	proof-quality	approved	claude/claude-opus-5-5	Both prior findings are fixed: the step that lifts a domination through the conditional expectation kernel is now hasCondMGFBound_cgf_of_ae_mgfDominatedOn, and the shared theorem tails are now measure_exists_le_mul_klBer_le_of_rateFunction. The remaining proofs are short, use no change/show or undocumented defeq, and their only repeats are one-line calls to shared lemmas.

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

_{Reviewing this diff at head b48ebdc. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.86.}