[RemyDegenne]

This PR derives the asymptotic part of [LS, Theorem 8.1] for the asymptotically optimal UCB algorithm ucbF σ2 as the Gaussian instance of KL-UCB for exponential families, as Bandits Layer 3.4 asks ("Deduce, as the Gaussian instance, the eventual form of Layer 2.2 for σ²-sub-Gaussian rewards"; Layer 2.2: "the eventual form is also the Gaussian instance of Layer 3.4"). Until now ucbF_regret_eventually_le and UCBF.integral_pullCount_eventually_le each had their own ε-argument over the explicit finite-time bound. Now they follow from klucbFam_gaussianReal (ucbF σ2 is KL-UCB for the Gaussian family of variance σ²):

• ucbF_regret_eventually_le is klucbFam_gaussianReal_regret_eventually_le with a common variance.
• UCBF.integral_pullCount_eventually_le is KLUCBFam.integral_pullCount_eventually_le for the Gaussian family, with d(μ_a, μ*) = Δ_a² / (2σ²) (expFamilyDiv_gaussianReal).

Both keep their names and their exact statements. They move from LMLExplore/Bandits/AsymptoticallyOptimalUCB.lean to LMLExplore/Bandits/KLUCB.lean, the first file where the KL-UCB family theorems exist; KLUCB.lean already imports AsymptoticallyOptimalUCB.lean. Their old proofs are deleted. The explicit finite-time bounds UCBF.integral_pullCount_le and ucbF_regret_le stay where they are, since Layer 2.2 says "the explicit constants above keep the proof through [LS, Lemma 8.2]". The module docstrings of both files are updated. AsymptoticallyOptimalUCB.lean drops its import of LMLExplore.Bandits.Regret, which only the moved proof used. The only downstream user is Bandits/AsymptoticOptimality.lean (UCBF.isConsistent, tendsto_ucbF_regret_div_log_gaussianBandit), which already imports KLUCB and builds unchanged.

Public declarations removed or renamed: none. The two moved theorems keep their names and statements; only their module changes, from LMLExplore.Bandits.AsymptoticallyOptimalUCB to LMLExplore.Bandits.KLUCB.

Milestone: Bandits Layer 3.4 (regret of KL-UCB for exponential families and its instances). After this PR, Layer 3 has only its completion examples left: the Bernoulli boundary level U(0, c) = 1 - e^{-c} and a two-armed Bernoulli bandit.

Verification (local checks, not CI): tauceti-local-checks verify --policy ordinary passed with scope: scoped: against 7fc78707241a5393aa85a7751e472cf1cb45fca9. The whole-library lake build --iofail succeeded (8551 jobs). local-axioms: checked 2 changed module(s), 64 declaration(s); 0 violation(s). Module-system, header-style and changed-module environment lint passed.

Roadmap: Bandits

🤖 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 moved theorems UCBF.integral_pullCount_eventually_le and ucbF_regret_eventually_le keep their exact statements in an equivalent variable context and are now derived from the Gaussian KL-UCB results with no added hypotheses. The new helpers (d(μ_a, μ*) = Δ_a²/(2σ²), and domination of sub-Gaussian X by the Gaussian member of mean a) are correctly stated for every base mean m.
✅	reuse	approved	claude/claude-opus-5-5	The moved theorems UCBF.integral_pullCount_eventually_le and ucbF_regret_eventually_le now come directly from KLUCBFam.integral_pullCount_eventually_le and klucbFam_gaussianReal_regret_eventually_le, and their old proofs are deleted. The two new helpers have no existing equivalent in LMLExplore, each has two users, and both are built on existing Gaussian exponential-family lemmas.
✅	scope	approved	claude/claude-opus-5-5	Single-topic refactor that re-proves the existing theorems ucbF_regret_eventually_le and UCBF.integral_pullCount_eventually_le as the Gaussian instance of KL-UCB, as Bandits Layers 2.2 and 3.4 require (README.md:305, :382). The new helpers expFamilyDiv_gaussianReal_eq_gap_sq and mgfDominatedOn_expFamily_natParam_gaussianReal are extracted from proof steps that were already inline, so they add no new capability.
✅	attribution	approved	claude/claude-opus-5-5	The moved theorems keep their [LS, (8.2)] / [LS, Theorem 8.1] citations, and the [LS] reference in KLUCB.lean now covers Chapters 8 and 10; the new helper lemmas are routine combinations of existing declarations in this repository. The roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The two eventual-regret theorems move to KLUCB.lean under their old names, with no compatibility leftovers, and the general sub-Gaussian ⇒ MGF-dominated lemma now sits in its probability home (ExponentialFamily/Gaussian.lean). The new KLUCB lemma expFamilyDiv_gaussianReal_eq_gap_sq is bandit-specific (it uses gap and bestArm), so it is correctly placed.
✅	generality	approved	claude/claude-opus-5-5	Both eventual ucbF bounds are now Gaussian instances of the general KL-UCB family theorems, which removes the special-case ε-argument. The new helpers are stated generally (any base mean m, any X/Q) and are each reused, and the moved theorems keep their standard-model hypotheses.
✅	placement	approved	claude/claude-opus-5-5	The eventual-regret theorems for ucbF move to KLUCB.lean, next to klucbFam_gaussianReal and the KL-UCB family theorems they now instantiate, with no forwarding surface left; the Gaussian domination helper sits in ExponentialFamily/Gaussian.lean and the bandit-specific divergence lemma in KLUCB.lean. The dropped Bandits.Regret import was used only by the deleted proof, and the new MGF.Bound import is needed for HasSubgaussianMGF.mgfDominatedOn_gaussianReal.
✅	naming	approved	claude/claude-opus-5-5	The two new helpers, HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal (dot notation on a Mathlib type) and expFamilyDiv_gaussianReal_eq_gap_sq (an equality conclusion), extend the existing mgfDominatedOn_gaussianReal and expFamilyDiv_gaussianReal names and describe their conclusions. The moved theorems keep names consistent with the adjacent *_eventually_le family, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The docstrings of the moved theorems and the two new helper lemmas are accurate and match their statements without overclaiming. Both module docstrings are updated consistently: AsymptoticallyOptimalUCB points to KLUCB for the asymptotic bounds with no stale text left, and KLUCB lists the moved theorems and cites Chapter 8.
✅	proof-quality	approved	claude/claude-opus-5-5	The Gaussian MGF-dominance fact and the identity d(μ_a, μ*) = Δ_a²/(2σ²) are each one shared lemma used at every site. The moved theorems are short instantiations that rewrite through the proven equation klucbFam_gaussianReal, with no brittle rewrite chains or undocumented definitional equality.

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

_{Reviewing this diff at head 74c8676. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.99.}