[RemyDegenne]

MGFDominatedAbove and MGFDominatedBelow become a single predicate, MGFDominatedOn X P Y Q Λ: domination at every parameter t ∈ Λ. Domination above is the case Λ = Set.Ici 0, domination below the case Set.Iic 0, and two-sided statements use Set.univ. The set of parameters is named Λ, as in HasMGFBound (#188).

Probability/Moments/MGF/Dominated.lean:

• MGFDominatedOn is the old structure with t ∈ Λ in place of 0 ≤ t or t ≤ 0, so the meaning is unchanged, including when Q is not a probability measure.
• API:
  • mono, a new lemma: domination on Λ implies domination on every subset;
  • mgfDominatedOn_union (an iff), MGFDominatedOn.union and MGFDominatedOn.univ_of_Iic_of_Ici, new: domination on Λ ∪ Λ' is domination on Λ and on Λ', so the one-sided producers on Set.Ici 0 and Set.Iic 0 combine into the Set.univ hypothesis of the two-sided consumers;
  • neg, generalized: -X is dominated by -Y on -Λ;
  • trans;
  • IdentDistrib.mgfDominatedOn, for every Λ.
• The lemmas on independent sums (integrable_exp_mul_sum_of_mgfDominatedOn, mgf_sum_le_pow_of_mgfDominatedOn) are one pair instead of two, for any t ∈ Λ, with no sign condition. The proof only uses t ≠ 0, so the lower-tail version no longer goes through neg.
• The Chernoff bounds take t ∈ Λ together with 0 ≤ t (upper tail) or t ≤ 0 (lower tail).

Bridge to HasMGFBound: mgfDominatedAbove_iff_hasMGFBound and mgfDominatedBelow_iff_hasMGFBound become one lemma, mgfDominatedOn_iff_hasMGFBound : MGFDominatedOn X P Y Q Λ ↔ HasMGFBound X (cgf Y Q) (Λ ∩ integrableExpSet Y Q) P.

Producers:

• mgfDominatedOn_Ici_bernoulliMeasure (mean at most q) and mgfDominatedOn_Iic_bernoulliMeasure (mean at least q). They have different hypotheses on the mean, so they stay two lemmas.
• The private Gaussian pair in GaussianThreshold.lean becomes one lemma on Set.univ.

Consumers:

• The exponential-family Chernoff bounds and the bounds in the reward stream take Set.Ici 0 or Set.Iic 0.
• The two-sided statements take one hypothesis hν : … Set.univ instead of hν_above and hν_below: forced exploration, D- and C-tracking, the deviations of empirical means, and the Track-and-Stop theorems.

No old name remains, and there are no aliases. The docstrings say "dominated on Set.Ici 0" and so on.

The companion roadmap change, LeanMachineLearning/LMLRoadmaps#15, updates the names that the Identification and Bandits roadmaps cite.

Checked locally:

• lake build --iofail;
• #lint in LMLExplore over the 10 changed modules passes.

Roadmap: Identification

🤖 Generated 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	MGFDominatedOn on Set.Ici 0 / Set.Iic 0 is by definition the old above/below predicate, and Set.univ is equivalent to having both. The general sum lemma is still correct at t = 0 when Q is not a probability measure, the Chernoff bounds keep their sign hypotheses, and no old name remains (grep finds nothing).
✅	reuse	approved	claude/claude-opus-5-5	Merges the duplicated Above/Below MGF-domination predicates and their lemma pairs into one MGFDominatedOn API, with no surviving old names, aliases or shims. New lemmas (mono, union, IdentDistrib.mgfDominatedOn) reuse Mathlib's mgf_congr_of_identDistrib and duplicate no existing material.
✅	scope	approved	claude/claude-opus-5-5	Single-topic refactor merging the already-merged MGFDominatedAbove/MGFDominatedBelow into MGFDominatedOn on a parameter set, with all callers updated; roadmap fit is automatic for reworked main material. The added mono/union lemmas are small API for the merged predicate, not new mathematical capability.
✅	attribution	approved	claude/claude-opus-5-5	Internal refactor merging MGFDominatedAbove/Below into MGFDominatedOn on a parameter set; it draws on no new external source and keeps the existing Boucheron–Lugosi–Massart, GK16 and DK19 credits.
✅	api-design	approved	claude/claude-opus-5-5	MGFDominatedOn replaces both one-sided predicates with no compatibility layer left; grep finds none of the old names in ./code. It now has mono, neg, trans, IdentDistrib.mgfDominatedOn, the bridge to HasMGFBound, and the new union lemmas, which close the previous gap between the one-sided Bernoulli results and the Set.univ hypothesis of the two-sided theorems.
✅	generality	approved	claude/claude-opus-5-5	The single MGFDominatedOn predicate on a parameter set Λ is the natural generalization: the sum lemmas need only t ≠ 0 and no longer duplicate the lower-tail proof through neg, and mono/neg/trans/union and the HasMGFBound bridge are stated for arbitrary Λ. The one-sided producers and Chernoff consumers sit on Set.Ici 0/Set.Iic 0 and the two-sided users on Set.univ, which is equivalent to the old pair of hypotheses, so no assumption was strengthened.
✅	placement	approved	claude/claude-opus-5-5	In-place refactor: the unified predicate, its new API and the HasMGFBound bridge stay in their existing canonical files, no files are added or moved, and no imports change. No old names or compatibility shims remain (grep for the old names over ./code returns nothing).
✅	naming	approved	claude/claude-opus-5-5	MGFDominatedOn and its API (mono, mgfDominatedOn_union, union, univ_of_Iic_of_Ici, neg, trans, IdentDistrib.mgfDominatedOn, mgfDominatedOn_iff_hasMGFBound, mgfDominatedOn_Ici/Iic_bernoulliMeasure) follow Mathlib's …On naming conventions, each name matches the strength of its statement, and dot-notation lemmas sit in the namespace of the Mathlib type they take. No old names remain in the code and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Module and declaration docstrings consistently describe the single MGFDominatedOn predicate on a parameter set Λ, and a repo-wide grep finds no remaining mentions of the removed names or of "dominated above/below". Each rewritten docstring matches its statement, including the t ∈ Λ plus sign hypotheses of the Chernoff bounds, the one-way neg on -Λ, and the Λ ∩ integrableExpSet bridge to HasMGFBound.
✅	proof-quality	approved	claude/claude-opus-5-5	The merged domination proofs are short and robust, and merging the predicates removes duplicated reasoning, including the lower-tail detour through neg. No undocumented change/show, brittle rewrite chains, or accidental definitional-equality steps were introduced.

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

_{Reviewing this diff at head 0730379. rubrics @ 32ce206. CLI @ 32ce206. Review spend: $9.96.}