[RemyDegenne]

Updates the names of LMLExplore's MGF domination predicates that the Identification and Bandits roadmaps cite, to follow LeanMachineLearning/LMLExplore#191. That PR replaces MGFDominatedAbove and MGFDominatedBelow with one predicate, MGFDominatedOn X P Y Q Λ, domination on a set Λ of parameters. Domination above is Set.Ici 0, below is Set.Iic 0, and two-sided is Set.univ.

Why. Workers follow the names the roadmaps cite, so the old ones would bring back the two parallel predicates.

Changes (LMLRoadmaps/Identification/, LMLRoadmaps/Bandits/):

• Identification:
  • the dependency table points to Probability/Moments/MGF/Dominated.lean (renamed by #188) and MGFDominatedOn;
  • Layer 1.2 (the Cramér–Chernoff bound with the rate function) says "dominated on [0, ∞)" and "on (−∞, 0]", and "on ℝ" for the two-sided bound. It drops the reference to the completed Refactors roadmap's form;
  • Layer 4.2: the unconditional MGF bound by cgf Y Q on Λ ∩ integrableExpSet Y Q is MGFDominatedOn X P Y Q Λ (mgfDominatedOn_iff_hasMGFBound), and sub-Gaussian variables are conditionally dominated on ℝ;
  • two docstrings in Suggested.lean.
• Bandits:
  • the table of LMLExplore material: MGFDominatedOn, mgfDominatedOn_Ici_bernoulliMeasure, mgfDominatedOn_Iic_bernoulliMeasure;
  • Layer 1.4's conditional Bernoulli domination;
  • the definition of an arm dominated by its family, "on ℝ".

Points to check

• This touches two roadmap directories, against the one-directory-per-PR convention, because it is a single rename across both. I can split it if you prefer.
• Merge it after refactor: one MGF domination predicate on a set of parameters LMLExplore#191, which introduces the cited names.
• Completed/Refactors/ keeps the old names: it records completed work.

Suggested.lean builds (lake build LMLRoadmaps.Identification.Suggested).

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

🤖 Generated with Claude Code