[RemyDegenne]

This PR defines Thompson sampling for exponential families with priors on the natural parameter, and the Jeffreys prior. It also proves that Gaussian Thompson sampling gaussianTS σ2 is the instance with the Gaussian family of variance σ² and its Jeffreys prior. This is the Bandits roadmap target Layer 5.1, Algorithm: "For families $(\rho_a)a$ of Layer 3 with log-partition functions $\psi_a=$ cgf id (ρ a) and priors $\pi_a$, σ-finite measures on $\Theta{\rho_a}$, define Thompson sampling. […] The Jeffreys prior is $\pi_J(d\theta)=\sqrt{\psi''(\theta)},d\theta$ on $\Theta_\rho$ [KKM13, Section 2]. Gaussian Thompson sampling with variance proxy $\sigma^2$ and flat prior (LMLExplore's gaussianTS […]) is the instance with the Gaussian family of variance $\sigma^2$ and its Jeffreys prior, a constant multiple of Lebesgue measure; define it as that instance." The names expFamilyTS and jeffreysPrior follow the roadmap's Suggested.lean.

Roadmap: Bandits

LMLExplore/Probability/Distributions/ExponentialFamily/Posterior.lean (new, 180 lines) holds the exponential-family part. Measure.expFamilyPosterior ρ T ν s S is the conjugate posterior of the natural parameter after s observations whose statistics sum to S. It is defined as (ν.withDensity fun θ ↦ exp (θ S - s ψ(θ)))[|Θ], with ψ = cgf T ρ and Θ the interior of integrableExpSet T ρ, so it works for any prior, improper ones included. The file proves expFamilyPosterior_apply, isProbabilityMeasure_expFamilyPosterior (normalizing constant positive and finite), isProbabilityMeasure_expFamilyPosterior_of_ne_zero, expFamilyPosterior_eq_zero_iff, an IsZeroOrProbabilityMeasure instance, expFamilyPosterior_smul (the posterior does not change when the prior is scaled) and measurable_expFamilyPosterior (measurable in S). It also defines Measure.jeffreysPrior ρ T, with its SigmaFinite instance. Mathlib's ProbabilityTheory.posterior is not reused: it is a kernel for a finite prior and is determined only up to null sets, while a sampling rule needs the posterior at every value of (s, S) and for improper priors.

ExponentialFamily/Gaussian.lean gets the Gaussian computations:

• iteratedDeriv_two_cgf_gaussianReal (ψ'' = v);
• jeffreysPrior_gaussianReal (the Jeffreys prior is √v • volume);
• expFamilyPosterior_gaussianReal_volume and expFamilyPosterior_gaussianReal_jeffreysPrior (the posterior is 𝒩((S - s m)/(s v), 1/(s v)), by completing the square);
• map_deriv_cgf_expFamilyPosterior_gaussianReal_jeffreysPrior (its image under the mean map is 𝒩(S/s, v/s)).

Probability/Moments/Basic.lean gets measurable_mgf and measurable_cgf for s-finite measures. These are not in Mathlib at the pinned version, and the measurability of the posterior in S needs them.

LMLExplore/Bandits/ThompsonSampling/Basic.lean (new, 233 lines) has the algorithm:

• expFamilyTSStackLaw ρ π s S: δ_⊤ if s = 0 or the posterior is 0, otherwise the image of the posterior by θ ↦ ψ'(θ) in EReal. It comes with _def, _zero, _of_expFamilyPosterior_eq_zero, _of_ne_zero, a probability instance and measurability.
• expFamilyTSLaw ρ π n h a, with _def, measurability and expFamilyTSLaw_history.
• expFamilyTS ρ π := perturbedLeaderAlgorithm …, for families and priors that are s-finite, with expFamilyTS_def.
• ExpFamilyTS.lintegral_pullCount_le: [LS, Theorem 36.2] for this algorithm against any stochastic bandit, in the reward-stack form, from PerturbedLeader.lintegral_pullCount_le.

Bandits/ThompsonSampling/Gaussian.lean proves gaussianTSStackLaw_eq_expFamilyTSStackLaw and gaussianTS_eq_expFamilyTS m hσ2. The second says that for σ2 ≠ 0, gaussianTS σ2 = expFamilyTS (fun a ↦ gaussianReal (m a) σ2) (fun a ↦ (gaussianReal (m a) σ2).jeffreysPrior id), for any base means m. gaussianTS is not redefined as the instance because the two differ at σ2 = 0. The Gaussian family of variance 0 is a Dirac family whose Jeffreys prior is 0, so every posterior is 0 and every perturbation is ⊤. gaussianTS 0, by contrast, samples δ_{μ̂}, and its existing lemmas (for example GaussianTS.pullCount_card_eq_one) hold for every σ2. This is the same pattern as klucbFam_gaussianReal … = ucbF σ2 in Layer 3.3.

To keep the generic definition upstream of its Gaussian instance, the existing Gaussian Thompson sampling file moves into a directory. Only imports and the module path change; no declaration is renamed or removed.

old module	new module
LMLExplore.Bandits.ThompsonSampling	LMLExplore.Bandits.ThompsonSampling.Gaussian

With this PR, Layer 5.1 is done except its Bernoulli completion example (the Jeffreys prior on the mean is Beta(1/2, 1/2)). What remains for Layer 5 is 5.3's [KKM13, Theorem 1]: the asymptotic regret of expFamilyTS with jeffreysPrior for bandits whose arms are members of one family. It will consume expFamilyTS, jeffreysPrior, expFamilyPosterior and ExpFamilyTS.lintegral_pullCount_le.

Sources: [KKM13] N. Korda, E. Kaufmann and R. Munos, Thompson sampling for 1-dimensional exponential family bandits, NeurIPS 2013, Section 2 (posterior and Jeffreys prior); [LS] Lattimore and Szepesvári, Bandit Algorithms, Chapter 36.

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

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The posterior, the Jeffreys prior, the perturbation laws and the Gaussian instance match [KKM13, Section 2], and the Gaussian posterior 𝒩((S−sm)/(sv),1/(sv)) and its mean-map image 𝒩(S/s,v/s) check out by hand against gaussianTSStackLaw (Gaussian.lean:121). Proving the equality with gaussianTS only for σ2 ≠ 0 is correct, because the two differ at σ2 = 0.
✅	reuse	approved	claude/claude-opus-5-5	The exponential-family posterior, Jeffreys prior, cond_smul, measurable_mgf/measurable_cgf and the Gaussian conjugate computations have no counterpart in Mathlib or LMLExplore (grep finds no scaling lemma among Mathlib's cond_* theorems and no mgf/cgf measurability lemma). The PR reuses cond, withDensity, cgf_gaussianReal, gaussianReal_map_const_mul/_add_const, perturbedLeaderAlgorithm and PerturbedLeader.lintegral_pullCount_le, and the module move leaves no forwarding shim.
✅	scope	approved	claude/claude-opus-5-5	Implements Bandits Layer 5.1 (expFamilyTS, jeffreysPrior, Gaussian Thompson sampling as the instance), with names matching the roadmap's Suggested.lean. The supporting lemmas (cond_smul, mgf/cgf measurability, Gaussian posterior computations), the 36.2 corollary and the module move are direct prerequisites or placement for that one target.
✅	attribution	approved	claude/claude-opus-5-5	The main informal sources, [KKM13, Section 2] for the posterior, Jeffreys prior and algorithm and [LS, Theorem 36.2 / Chapter 36] for the pull-count bound, are cited in the module and declaration docstrings of the new files. No vendored or closely adapted formal material was found (the pinned Mathlib has no measurable_mgf, cond_smul or Jeffreys declarations), and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The old LMLExplore.Bandits.ThompsonSampling module is gone with no forwarding import or alias left behind, and every new definition comes with a (rfl) _def lemma, case lemmas, instances and measurability, so callers never have to unfold. The general helpers (cond_smul, measurable_mgf, measurable_cgf) are public in their natural shared homes and are not in the pinned Mathlib (grep finds nothing).
✅	generality	approved	claude/claude-opus-5-5	The posterior, Jeffreys prior and measurability lemmas are stated for a general measure, statistic and s-finite prior, and the Gaussian Jeffreys-prior posterior and the gaussianTS instance are derived from them via expFamilyPosterior_smul and gaussianTSStackLaw_eq_expFamilyTSStackLaw. The assumptions (SFinite, AEMeasurable, c ∉ {0, ∞}, v ≠ 0, s ≠ 0) are all used, and cond_smul, measurable_mgf and measurable_cgf have no Mathlib counterpart (grep finds none).
✅	placement	approved	claude/claude-opus-5-5	Generic material (cond_smul, measurable_mgf/measurable_cgf, expFamilyPosterior, jeffreysPrior) lives in files matching its topic, the Gaussian instances sit in ExponentialFamily/Gaussian.lean, and the generic algorithm in ThompsonSampling/Basic.lean comes before ThompsonSampling/Gaussian.lean. The relocation updated the only in-repo import with no forwarding module, and every new import is used and narrowly scoped.
✅	naming	approved	claude/claude-opus-5-5	The new names describe their conclusions in standard terminology and match the roadmap's expFamilyTS/jeffreysPrior and the adjacent gaussianTS*/expFamily* declarations. expFamilyPosterior and jeffreysPrior sit correctly in MeasureTheory.Measure for dot notation on a measure, the suffixes match their statements, no notation is introduced, and nothing clashes with Mathlib (measurable_mgf, measurable_cgf and cond_smul have no matches in ./mathlib).
✅	documentation	approved	claude/claude-opus-5-5	Both earlier findings are fixed: the module docstrings in ThompsonSampling/Basic.lean and ExponentialFamily/Gaussian.lean now state the nonzero-variance hypothesis. Every new file has a module docstring and every public declaration has an accurate docstring.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, use robust tactics (fun_prop, simp, field_simp/ring), factor the reusable steps (cond_smul, deriv_cgf_gaussianReal_eq, measurable_cgf), and do not rely on undocumented definitional equality. The one longer rewrite chain, in expFamilyPosterior_gaussianReal_volume, has a comment explaining the completing-the-square step.

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

_{Reviewing this diff at head 8d5088b. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.87.}