[prevostad]

This PR proves the limit form of [KKM13, Theorem 1] for Thompson sampling with the Jeffreys prior, E[R_n] / log n → ∑_{a : Δ_a > 0} Δ_a / d(μ_a, μ*), together with its Bernoulli instance. This is the statement of Bandits Layer 5.3 ("Frequentist regret"): an upper bound in eventual form, matched by the Lai–Robbins lower bound of Layer 4.4. It also covers the completion check that "the asymptotic constants of Layers 3 and 5 coincide with the Lai–Robbins constants of Layer 4.4 … in particular for Gaussian and Bernoulli arms". The upper bound expFamilyTS_jeffreysPrior_regret_eventually_le (#320) and the Gaussian limit tendsto_gaussianTS_regret_div_log_gaussianBandit were already on main. Until now, main had no limit statement for Jeffreys-prior Thompson sampling on any non-Gaussian family.

Roadmap: Bandits

Added to LMLExplore/Bandits/AsymptoticOptimality.lean, next to the analogous KL-UCB statements (klucbFam_regret_eventually_le_of_mem_image_expFamily, KLUCBFam.isConsistent, tendsto_klucbFam_regret_div_log):

• expFamilyTS_jeffreysPrior_regret_eventually_le_of_mem_image_expFamily: the upper bound of feat: asymptotic optimality of Thompson sampling with the Jeffreys prior [KKM13, Theorem 1] #320 for bandits whose arm laws are members of the families. The domination and nondegeneracy hypotheses are discharged here, because each arm is its own member of mean μ_a.
• expFamilyTS_jeffreysPrior_regret_eventually_le_of_common_means: the same bound for families with a common set of means, proper Jeffreys posteriors and Jeffreys priors finite below every mean; the consistency and limit theorems below both use it.
• ExpFamilyTS.isConsistent_jeffreysPrior: consistency over those bandits, for families with a common set of means, Jeffreys posteriors that are proper after some observations, and Jeffreys priors that are finite on {θ | ψ'(θ) ≤ m} for every mean m.
• tendsto_expFamilyTS_jeffreysPrior_regret_div_log and isLittleO_expFamilyTS_jeffreysPrior_regret_sub_mul_log: [KKM13, Theorem 1], through eventually_mul_log_le_integral_regret_expFamily.
• tendsto_expFamilyTS_jeffreysPrior_regret_div_log_bernoulliBandit and isLittleO_…_bernoulliBandit: the Bernoulli instance, on Bernoulli bandits with means in (0, 1). It uses the Beta(1/2, 1/2) Jeffreys prior, and its constant is written (klBer (p a) (⨆ b, p b)).toReal, as in tendsto_klucb_regret_div_log_bernoulliBandit.

Added to LMLExplore/Probability/Distributions/ExponentialFamily/Chernoff.lean:

• ProbabilityTheory.mgfDominatedOn_expFamily_natParam_integral_of_mem_image: a member of an exponential family is dominated on every set by the member of its mean. Both the existing KL-UCB wrapper klucbFam_regret_eventually_le_of_mem_image_expFamily and the new Thompson-sampling wrapper use it instead of repeating the proof inline.

Added to LMLExplore/Probability/Distributions/ExponentialFamily/Bernoulli.lean, which the Bernoulli instance needs:

• the instance isFiniteMeasure_jeffreysPrior_bernoulliMeasure_sigmoid: the Jeffreys prior has total mass π;
• isProbabilityMeasure_expFamilyPosterior_bernoulliMeasure_sigmoid_jeffreysPrior: the Jeffreys posteriors are probability measures for -1/2 < S < s + 1/2.

No declarations are removed or renamed.

After this PR, Layer 5.3 remains open only for families whose Jeffreys prior is infinite below the optimal mean, such as exponential arms. The module docstring of ThompsonSampling/Optimality.lean explains why the [LS, Theorem 36.2] route fails there. The other open Bandits item, Layer 6.1, is covered by the open PR #323.

🤖 Prepared with Claude Code

[prevostad]

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

The new Jeffreys-TS limit, consistency and Bernoulli results are new material that reuses the existing upper bound, Lai–Robbins and KL-UCB plumbing. However, the upper-bound wrapper copies the non-degeneracy and MGF-domination proof block of the KL-UCB wrapper line for line.

• LMLExplore/Bandits/AsymptoticOptimality.lean:441 — In expFamilyTS_jeffreysPrior_regret_eventually_le_of_mem_image_expFamily, the hρ/hρs/hdom block (lines 441-452) copies lines 296-307 of klucbFam_regret_eventually_le_of_mem_image_expFamily line for line (not_ae_eq_const_of_gap_pos ×2, rw [Measure.expFamily_natParam_integral_of_mem_image ha (hν a)], (IdentDistrib.refl aemeasurable_id).mgfDominatedOn). Fix: Move this block into one shared lemma in the ExpFamily section, e.g. mgfDominatedOn_expFamily_natParam_of_mem_image (hν) (ha : ∀ c, ¬ id =ᵐ[ρ a] fun _ ↦ c) Λ : MGFDominatedOn id (ν a) id ((ρ a).expFamily id ((ρ a).natParam id (ν a)[id])) Λ. Call it from both wrappers, and inline not_ae_eq_const_of_gap_pos at the call sites.

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 · 28s · 130.6k in (96k cache read, 34.6k cache write) / 2.6k out tokens · reviewing this diff · rubric}

[prevostad]

🟡 proof-quality — request_changes claude/claude-opus-5-5

Proofs are short and avoid undocumented defeq tricks, but the step from the family-wide hypotheses (hM, hπ) to the hypotheses of the arm-wise upper bound is written out twice inline instead of being a lemma.

• LMLExplore/Bandits/AsymptoticOptimality.lean:473 — ExpFamilyTS.isConsistent_jeffreysPrior and tendsto_expFamilyTS_jeffreysPrior_regret_div_log (lines 501-507) both rebuild hμs/hμb via hM (bestArm ν) a ▸ hμ _ / hM a (bestArm ν) ▸ hμ a, fun a _ ↦ hprop a, and hπs via ne_top_of_le_ne_top (hπ _ _ (hμ _)) (measure_mono fun _ hθ ↦ le_trans hθ hm.le) before calling expFamilyTS_jeffreysPrior_regret_eventually_le_of_mem_image_expFamily; the reusable fact (common means plus a finite prior below every mean give the regret bound) is never stated. Fix: Add a lemma (e.g. expFamilyTS_jeffreysPrior_regret_eventually_le_of_common_means) taking hM hprop hπ hν h hc and returning the eventual c log n bound, and use it in both theorems (the hμs local in tendsto_… is still needed for eventually_mul_log_le_integral_regret_expFamily).

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 · 20s · 47.6k in (41.9k cache read, 5.7k cache write) / 1.9k out tokens · reviewing this diff · rubric}

[prevostad]

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.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The new upper bound, consistency, limit and little-o statements match [KKM13, Theorem 1] and the existing Lai–Robbins constant, and their hypotheses are no stronger than those of the underlying theorems already on main. The Bernoulli facts (prior total mass π, proper posteriors for -1/2 < S < s + 1/2) are proved from the existing Beta pushforward lemmas, not assumed.
🟡	reuse	changes requested	claude/claude-opus-5-5	The new Jeffreys-TS limit, consistency and Bernoulli results are new material that reuses the existing upper bound, Lai–Robbins and KL-UCB plumbing. However, the upper-bound wrapper copies the non-degeneracy and MGF-domination proof block of the KL-UCB wrapper line for line.
✅	scope	approved	claude/claude-opus-5-5	The PR proves Bandits Layer 5.3 itself ([KKM13, Theorem 1] limit for Jeffreys-prior Thompson sampling) plus its Bernoulli completion example, with only the two small Bernoulli Jeffreys-prior lemmas it needs. It is a single coherent topic that advances the roadmap target directly.
✅	attribution	approved	claude/claude-opus-5-5	The central informal source [KKM13] (Theorem 1, Figure 1) is cited in the references and theorem docstrings of both touched files, and the Lai–Robbins constant is already credited to [BK96]; the new Bernoulli lemmas are routine and need no further credit.
✅	api-design	approved	claude/claude-opus-5-5	The new exponential-family and Bernoulli Thompson-sampling statements use the same names and structure as the KL-UCB statements in the same file. The two supporting Bernoulli results are needed by the Bernoulli theorem, and the PR adds no compatibility layer and exposes no definition bodies.
✅	generality	approved	claude/claude-opus-5-5	The exponential-family Thompson-sampling statements reuse the hypotheses of the KL-UCB versions and add only the two Jeffreys-specific ones (proper posteriors, prior finite below each mean), and the Bernoulli theorems are derived from the general one. The (0, 1) restriction on Bernoulli means is needed because this exponential family only covers means strictly between 0 and 1.
✅	placement	approved	claude/claude-opus-5-5	The Jeffreys-prior Thompson sampling limits sit in AsymptoticOptimality.lean next to the Gaussian Thompson sampling and KL-UCB family limits, which they need because they use LaiRobbins, and the new import of ThompsonSampling.Optimality is required for expFamilyTS_jeffreysPrior_regret_eventually_le. The Bernoulli Jeffreys finiteness and posterior lemmas sit in the existing Jeffreys section of ExponentialFamily/Bernoulli.lean, next to the result they come from.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions and mirror the adjacent KL-UCB and Bernoulli declarations (klucbFam_regret_eventually_le_of_mem_image_expFamily, KLUCBFam.isConsistent, tendsto_klucb_regret_div_log_bernoulliBandit); ExpFamilyTS is the project's own namespace and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Every new theorem and the exported instance have docstrings that match their hypotheses (common means, proper Jeffreys posteriors, finite Jeffreys priors on {θ | ψ'(θ) ≤ m}) and conclusions, and the total-mass π claim matches map_deriv_cgf_jeffreysPrior_bernoulliMeasure_sigmoid. The module docstring and Main statements entries are updated accurately, the KKM13 reference is added, and neither file's docstrings mention roadmap layers or project process.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	Proofs are short and avoid undocumented defeq tricks, but the step from the family-wide hypotheses (hM, hπ) to the hypotheses of the arm-wise upper bound is written out twice inline instead of being a lemma.

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

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