[RemyDegenne]

This PR adds the exponential-rewards completion example of KL-UCB for exponential families, together with its gamma generalization. It computes the extended divergence (the Cramér rate function) of the gamma family of known shape at every real level and the KL-UCB upper confidence level it determines. It then deduces that KL-UCB is asymptotically optimal on bandits with gamma arms of known, possibly different, shapes, and on bandits with exponential arms.

Roadmap target: Bandits, Layer 3 (KL-UCB for exponential families), the completion example "exponential rewards (expMeasure, d(x,q)=x/q−1−log(x/q))". It is also an instance of Layer 4.5, the asymptotic optimality of KL-UCB for families with a common set of means, here (0, ∞). After this PR, the remaining Layer 3 completion examples are the Bernoulli boundary level U(0,c)=1−e^{−c} and the two-armed Bernoulli bandit.

Roadmap: Bandits

New declarations (none removed or renamed):

• ExponentialFamily/Gamma.lean:
  • image_expFamily_gammaMeasure: the members are the gammaMeasure a b, b > 0.
  • expFamilyRate_gammaMeasure: dbar(x, μ) = a (x/μ − 1 − log(x/μ)) for x > 0.
  • expFamilyRate_gammaMeasure_of_nonpos: dbar = ∞ for x ≤ 0. This uses Tau Ceti's ae_pos_gammaMeasure and rateFunction_eq_top_of_ae_gt.
  • le_expFamilyUpper_gammaMeasure_iff: q ≤ U(x, c) ↔ a (x/q − 1 − log(x/q)) ≤ c, for 0 < x ≤ q. This is the KL-UCB index.
  • expFamilyUpper_gammaMeasure_of_nonpos: U(x, c) = x for x ≤ 0 and finite c.
• ExponentialFamily/Exponential.lean: the shape-1 corollaries image_expFamily_expMeasure, expFamilyRate_expMeasure, expFamilyRate_expMeasure_of_nonpos, le_expFamilyUpper_expMeasure_iff and expFamilyUpper_expMeasure_of_nonpos.
• Bandits/AsymptoticOptimality.lean:
  • tendsto_klucbFam_gammaMeasure_regret_div_log and isLittleO_klucbFam_gammaMeasure_regret_sub_mul_log: for arms gammaMeasure (κ a) (r a) and KL-UCB for the families generated by any gammaMeasure (κ a) (s a), E[R_n]/log n → Σ_{Δ_a>0} Δ_a / (κ_a (μ_a/μ* − 1 − log(μ_a/μ*))), the Lai–Robbins constant.
  • tendsto_klucbFam_expMeasure_regret_div_log and isLittleO_klucbFam_expMeasure_regret_sub_mul_log: the exponential instance.

The bandit statements specialize the existing tendsto_klucbFam_regret_div_log, the same way as its Gaussian instance tendsto_klucbFam_gaussianReal_regret_div_log. No Mathlib infrastructure is vendored.

Local checks (not CI): lake build --iofail succeeded. The shared verification reported scope: scoped: against da012591023b4d03a800af6fd377bc7c9b231392 and local-axioms: checked 3 changed module(s), 61 declaration(s); 0 violation(s), and the module-system, header and environment-lint checks passed.

🤖 Prepared with Claude Code

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

[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 gamma and exponential rate-function and upper-confidence-level statements match the definitions of expFamilyRate and expFamilyUpper at both positive and nonpositive levels, and the bandit theorems specialize tendsto_klucbFam_regret_div_log with the correct Lai–Robbins constant κ_a(μ_a/μ* − 1 − log(μ_a/μ*)). No mis-formalization, vacuity or content hidden in hypotheses found.
✅	reuse	approved	claude/claude-opus-5-5	The gamma-family rate function, upper confidence level, member image and KL-UCB optimality instances are new; their proofs reuse the existing general lemmas (expFamilyRate_eq_ofReal_expFamilyDiv, rateFunction_eq_top_of_ae_gt, le_expFamilyUpper_iff, expFamilyUpper_le_iff, tendsto_klucbFam_regret_div_log). The exponential corollaries follow the file's existing shape-1 pattern (klDiv_expMeasure) and are not redundant wrappers.
✅	scope	approved	claude/claude-opus-5-5	Completes the Bandits Layer 3 example 'exponential rewards (expMeasure, d(x,q)=x/q-1-log(x/q))' (roadmap/LMLRoadmaps/Bandits/README.md:389) through its gamma known-shape generalization and the matching KL-UCB optimality instance, as one coherent unit. No scope findings.
✅	attribution	approved	claude/claude-opus-5-5	The gamma/exponential rate-function, upper-confidence and asymptotic-optimality results specialize existing KL-UCB results whose module docstrings already cite [GC11; CGMMS13; LS], and the Gamma/Exponential files already cite Garivier–Kaufmann for these arm models. Nothing is vendored or closely adapted, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The new gamma/exponential rate-function, upper-confidence and KL-UCB optimality results are public theorems with no exposed bodies or compatibility surface, and their names and @[simp] annotations match the existing Gaussian and Bernoulli instances. expMeasure is a plain Mathlib def that simp does not unfold, so the exponential simp lemmas can fire, and the iff characterization is the right API for an upper confidence level with no closed form.
✅	generality	approved	claude/claude-opus-5-5	The gamma lemmas are stated once at the natural level of a known shape and use every hypothesis; the exponential lemmas and the bandit theorems are derived from them and from the general KL-UCB theorem, without repeating any proof.
✅	placement	approved	claude/claude-opus-5-5	The gamma and exponential rate-function and upper-confidence lemmas live in their family files, like the Gaussian ones in ExponentialFamily/Gaussian.lean, and the bandit instances sit next to the Gaussian KL-UCB instance in AsymptoticOptimality.lean. Gamma.lean's switch from Mean to UpperConfidence is required by the new expFamilyUpper and expFamilyRate lemmas and matches Gaussian.lean and Bernoulli.lean, and no import is unused or too broad.
✅	naming	approved	claude/claude-opus-5-5	New names follow the established sibling patterns (image_expFamily_, expFamilyRate_, le_expFamilyUpper_iff, expFamilyUpperof_nonpos, tendsto_klucbFam*_regret_div_log) and match statement strength. No new notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Every new declaration and module-docstring entry is documented accurately and in the same style as the existing Gaussian instance. The earlier inaccuracy at x = 0 in expFamilyRate_gammaMeasure_of_nonpos is fixed: the docstring now rests on the almost-sure strict positivity of gamma laws.
✅	proof-quality	approved	claude/claude-opus-5-5	The new proofs are short, explicit specializations of existing gamma-family, rate-function and KL-UCB results, with no change/show or accidental defeq. expMeasure is unfolded through its Mathlib definition, as the file's existing lemmas already do, and the single bounded convert has a comment and is closed by one rewrite.

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

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