[RemyDegenne]

Amends the Identification roadmap, Layer 1.2, so that exponential families take a probability measure ρ on any measurable space 𝓧 and a measurable statistic T : 𝓧 → ℝ, as ρ.expFamily T η = ρ.tilted (fun x ↦ η * T x). The natural exponential families of measures on ℝ are the case T = id. Companion to #5 (the Refactors roadmap, Layers 0.2 and 0.3, which restate the merged exponential-family code in this generality).

Why. The roadmap's identification tasks already take observations in any measurable space. Exponential families fixed to ℝ with the identity statistic would make every later layer built on them, from GLR statistics and deviation inequalities to Track-and-Stop, live in the narrower setting. The proofs work unchanged with a statistic T. Mathlib's cgf, tilted and LMLExplore's strictMonoOn_deriv_cgf are already stated for a general random variable.

Changes (only LMLRoadmaps/Identification/):

• 1.2 setting. Measures on 𝓧 with a statistic T; ψ = cgf T ρ; strict monotonicity when T is not ρ-a.e. constant. The names are expFamily, expFamilyMeans, natParam and expFamilyDiv.
• Instances. Poisson is stated on ℕ with T = Nat.cast, Mathlib's native poissonMeasure, with no pushforward. The Gaussian laws of known mean m are added as a family with T x = (x - m)², means the variances v, and d(v, v') = (v/v' - 1 - log(v/v'))/2. These two give the generality concrete uses.
• Cramér–Chernoff. The bound takes the dominated form of Refactors Layer 0.3. That form contains the Bandits Layer 1.4 bound, which the old wording claimed to generalize but didn't.
• Bandit of a mean vector. Per-arm families (ρ_a, T_a) on a common observation space.
• Titles and suggested homes now say "exponential families".
• Suggested.lean. natExpFamily/klDiv_natExpFamily become expFamily/klDiv_expFamily, and the Track-and-Stop signature uses expFamily (ρ a) id η.

Suggested.lean builds.

Drafted with Claude Opus 5.5 at the request of the code owner.

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1