Identification, Bandits: MGFDominatedOn in place of MGFDominatedAbove and MGFDominatedBelow

LMLRoadmaps/Bandits/README.md

@@ -153,7 +153,7 @@ dependency versions used to check the interfaces (LML `53be244`, Mathlib `2e318f
 | Convex analysis | LML [`Bregman/Basic.lean`][lml-breg] (`bregDiv`, notation `D_[f](x, y, J)`, `bregDiv_three_point`), [`Subgradient/`][lml-subgrad]; Tau Ceti [`Conjugate.lean`][tc-conj] (`fenchelConjugate`, for a bilinear pairing), [`Strong.lean`][tc-strong] (`StrongConvexOn.add_add_le_of_hasFDerivWithinAt`); Mathlib `StrongConvexOn`, `PiLp`; LMLExplore `simplex` (`Analysis/Convex/Simplex.lean`) |
 | Linear algebra | Mathlib `ContinuousLinearMap.IsPositive` and its Loewner order, `LinearMap.det`, `Matrix.det_one_add_replicateCol_mul_replicateRow`, `Matrix.add_mul_mul_inv_eq_sub`; Tau Ceti [`Frame.lean`][tc-frame] (`frameOperator`), [`AffineNormalization.lean`][tc-affine] (`IsCompact.exists_affineBasis_abs_coord_le_one`) and [`MoorePenrose.lean`][tc-mp] (`LinearMap.moorePenroseInverse`, `LinearMap.IsMoorePenroseInverse`, `LinearEquiv.moorePenroseInverse_eq_symm`) |
 | Designs | Mathlib `Convexity.StdSimplex` (finitely supported probability weights; `StdSimplex.map`, `StdSimplex.range_toFun_comp_weights`) |
-| LMLExplore material that the general forms below extend | exponential families (`Probability/Distributions/ExponentialFamily/`: `Measure.expFamily`, `expFamilyMeans`, `natParam`, `expFamilyDiv`), MGF domination (`MGFDominatedAbove`, `MGFDominatedBelow`, `mgfDominatedAbove_bernoulliMeasure`, `mgfDominatedBelow_bernoulliMeasure`), the Bandits algorithms `ucbF`, `klucb`, `gaussianTS`, `exp3`, `exp3IX`, `exp4` and the lower-bound files, follow-the-perturbed-leader policies (`perturbedLeaderAlgorithm`, `PerturbedLeader.lintegral_pullCount_le`), the FTRL lemma `sum_apply_sub_le_ftrl` (time-varying regularizers), `ConvexOn.exists_mem_segment_apply_sub_sub_bregDiv_div_le` (second-order Bregman bound), `softmax_regret_le`, `IsUnbiasedRound`, `designOp`, `ridgeEstimate` |
+| LMLExplore material that the general forms below extend | exponential families (`Probability/Distributions/ExponentialFamily/`: `Measure.expFamily`, `expFamilyMeans`, `natParam`, `expFamilyDiv`), MGF domination (`MGFDominatedOn`, `mgfDominatedOn_Ici_bernoulliMeasure`, `mgfDominatedOn_Iic_bernoulliMeasure`), the Bandits algorithms `ucbF`, `klucb`, `gaussianTS`, `exp3`, `exp3IX`, `exp4` and the lower-bound files, follow-the-perturbed-leader policies (`perturbedLeaderAlgorithm`, `PerturbedLeader.lintegral_pullCount_le`), the FTRL lemma `sum_apply_sub_le_ftrl` (time-varying regularizers), `ConvexOn.exists_mem_segment_apply_sub_sub_bregDiv_div_le` (second-order Bregman bound), `softmax_regret_le`, `IsUnbiasedRound`, `designOp`, `ridgeEstimate` |
 
 The [Kiefer–Wolfowitz formalization in `colt-2026-83`][kw] (Apache-2.0, no `sorry`) proves the
 existence of G-optimal designs for compact spanning subsets of `EuclideanSpace ℝ ι`
@@ -263,8 +263,8 @@ against an environment with a single arm is $0$.
    supermartingale $\exp(\lambda S_t-\psi(\lambda)N_t)$ of a sum sampled along a predictable
    sequence, and Ville's inequality, as in the proof of [GC11, Theorem 10]) is that roadmap's
    Layer 4.2. Prove here the bounded instance: a random variable with values in $[0,1]$ whose
-   conditional mean given a σ-algebra is at most (at least) $m$ is conditionally dominated above
-   (below) by $\mathcal B(m)$ [GC11, Lemma 9; LS, Note 10.3.1], and the rate function of
+   conditional mean given a σ-algebra is at most (at least) $m$ is conditionally dominated by
+   $\mathcal B(m)$ on $[0,\infty)$ (on $(-\infty,0]$) [GC11, Lemma 9; LS, Note 10.3.1], and the rate function of
    $\mathcal B(m)$ at a level $p\in[0,1]$ is `klBer p m`. Deduce for i.i.d. $X_i\in[0,1]$ with mean
    $\mu$ [LS, Lemma 10.3]: $P(\hat\mu_n\ge\mu+\varepsilon)\le\exp(-n\,d(\mu+\varepsilon,\mu))$ for
    $\varepsilon\in[0,1-\mu]$ and the lower tail, the boundary levels $0$ and $1$ included, and
@@ -320,10 +320,10 @@ $\eta_\rho(q)=$ `ρ.natParam id q`), the divergence $d_\rho(x,q)=$ `ρ.expFamily
 $M_\rho\times M_\rho$, and its extension $\bar d_\rho(x,q)\in[0,\infty]$ to every level
 $x\in\mathbb R$, the Cramér–Chernoff rate function of $\rho_{(q)}$ at $x$. Each arm $a$ has its
 own family $\rho_a$. Arm $a$ is *dominated by its family* if its mean $\mu_a$ lies in
-$M_{\rho_a}$ and its law $\nu_a$ is MGF-dominated above and below by $\rho_{a,(\mu_a)}$
-(LMLExplore's `MGFDominatedAbove`, `MGFDominatedBelow`). Laws on $[0,1]$ with mean in $(0,1)$ are
-dominated by the Bernoulli family (`mgfDominatedAbove_bernoulliMeasure`,
-`mgfDominatedBelow_bernoulliMeasure`), σ²-sub-Gaussian laws by the Gaussian family of variance
+$M_{\rho_a}$ and its law $\nu_a$ is MGF-dominated by $\rho_{a,(\mu_a)}$ on $\mathbb R$
+(LMLExplore's `MGFDominatedOn` with `Set.univ`). Laws on $[0,1]$ with mean in $(0,1)$ are
+dominated by the Bernoulli family (`mgfDominatedOn_Ici_bernoulliMeasure`,
+`mgfDominatedOn_Iic_bernoulliMeasure`), σ²-sub-Gaussian laws by the Gaussian family of variance
 $\sigma^2$ (Identification roadmap, Layer 4.2), and the members of a family by the family itself.
 
 1. **Upper confidence levels.** For a family $\rho$, $x\in\mathbb R$ and $c\in[0,\infty]$, define

LMLRoadmaps/Identification/README.md

@@ -64,7 +64,7 @@ generating functions with its exponential supermartingales (Layer 4.2).
 | Conditional means of the feedback and their martingale | LML `SequentialLearning/Means.lean` (`Environment.means`, `IsAlgEnvSeq.condExp_feedback`), `FeedbackMartingale.lean` (`noiseSum`, `IsAlgEnvSeq.martingale_noiseSum`) |
 | KL divergence of histories at a fixed horizon | LML `SequentialLearning/DivergenceDecomposition.lean` (`IsAlgEnvSeq.klDiv_map_history_stepKernel`, for any two algorithm-environment pairs); LMLExplore `Learning.IsAlgEnvSeq.klDiv_map_history_eq_sum_pullCount`, `Learning.klDiv_stoppedHistMeasure_le` |
 | Binary relative entropy, Bretagnolle–Huber, Ville's inequality, mixtures of supermartingales, time-uniform sub-Gaussian bounds, Chernoff bounds in relative-entropy form | LMLExplore (Bandits roadmap, Layers 0.2, 1 and 4): `klBer`, `klBerReal`, `exp_neg_klDiv_div_two_le`, `MeasureTheory.Supermartingale.measure_exists_le_le`, `supermartingale_integral_of_integrable`, `supermartingale_exp_sum_mul_of_hasCondSubgaussianMGF`, `measureReal_sum_ge_le_exp_klBerReal` |
-| Sub-Gaussian and sub-exponential random variables, unconditional and conditional | Mathlib `Probability/Moments/SubGaussian.lean` (`HasSubgaussianMGF`, `Kernel.HasSubgaussianMGF`, `HasCondSubgaussianMGF`), LML `ForMathlib/Probability/Moments/SubExponential.lean` (`HasSubexponentialMGF`, `HasCondSubexponentialMGF`); LMLExplore `Probability/Moments/MGFDominated.lean` (`MGFDominatedAbove`, `MGFDominatedBelow`) |
+| Sub-Gaussian and sub-exponential random variables, unconditional and conditional | Mathlib `Probability/Moments/SubGaussian.lean` (`HasSubgaussianMGF`, `Kernel.HasSubgaussianMGF`, `HasCondSubgaussianMGF`), LML `ForMathlib/Probability/Moments/SubExponential.lean` (`HasSubexponentialMGF`, `HasCondSubexponentialMGF`); LMLExplore `Probability/Moments/MGF/Dominated.lean` (`MGFDominatedOn`) |
 | Design operators, self-normalized bounds, G-optimal designs | Bandits roadmap, Layer 8 (`designOp`, the design operator $V(\pi)$ of a design, the self-normalized bound, the Kiefer–Wolfowitz theorem); Tau Ceti `Analysis/InnerProductSpace/Frame.lean` (`frameOperator`) |
 | Exponential weights, regret of online linear optimization | Bandits roadmap, Layer 6 |
 | KL divergence, chain rule, data processing, exponential tilting, cumulant generating functions | Mathlib `InformationTheory/KullbackLeibler/`, `MeasureTheory/Measure/Tilted.lean`, `MeasureTheory/Measure/LogLikelihoodRatio.lean`, `Probability/Moments/` (`cgf`, `integrableExpSet`, `deriv_cgf`, `iteratedDeriv_two_cgf`) |
@@ -363,16 +363,16 @@ forms above, and that development may be adapted to them.
      Layer 1.4). Prove that $\bar d$ is continuous on (closure of the means)$\times$(means) as an
      `ℝ≥0∞`-valued function.
    - Prove the Cramér–Chernoff bound with the rate function: for independent real random variables
-     $X_i$, $i\in s$, each dominated above by a real random variable $X$ (LMLExplore's
-     `MGFDominatedAbove`, the Refactors roadmap's Layer 0.3 form), every $x\ge\mathbb E[X]$ and
-     every real $r\le I_X(x)$, $P\big(\sum_{i\in s}X_i\ge\#s\,x\big)\le\exp(-\#s\,r)$; and the lower
-     tail for variables dominated below and $x\le\mathbb E[X]$. For $X$ the statistic under the
+     $X_i$, $i\in s$, each dominated on $[0,\infty)$ by a real random variable $X$ (LMLExplore's
+     `MGFDominatedOn X_i P X Q (Set.Ici 0)`), every $x\ge\mathbb E[X]$ and every real
+     $r\le I_X(x)$, $P\big(\sum_{i\in s}X_i\ge\#s\,x\big)\le\exp(-\#s\,r)$; and the lower tail for
+     variables dominated on $(-\infty,0]$ and $x\le\mathbb E[X]$. For $X$ the statistic under the
      member of mean $\mu$, this is the bound $\exp(-\#s\,\bar d(x,\mu))$ at every level $x\ge\mu$,
      not only at the means; it contains LMLExplore's
      `iIndepFun.measureReal_sum_ge_le_exp_expFamilyDiv` and the Bandits roadmap's Layer 1.4 bound,
      boundary levels included.
    - Deduce the two-sided bound $P\big(\#s\,\bar d(\hat\mu_s,\mu)\ge z\big)\le2e^{-z}$ for every
-     $z\ge0$, for the empirical mean $\hat\mu_s$ of variables dominated above and below by the
+     $z\ge0$, for the empirical mean $\hat\mu_s$ of variables dominated on $\mathbb R$ by the
      member of mean $\mu$.
    - Prove the sub-Gaussian comparison: $d(\mu,\mu')\ge(\mu-\mu')^2/(2\sigma^2)$ when the family has
      variance at most $\sigma^2$ on the segment.
@@ -695,14 +695,14 @@ alternatives, and Gaussian costs with arm-dependent variances in design-operator
        and LML's `HasCondSubexponentialMGF m hm X V b μ` the case $\psi(t)=Vt^2/2$ on
        $\{t:b|t|\le1\}$;
      - the unconditional version with $\psi$ the cumulant generating function of a real random
-       variable $Y$ on $[0,\infty)\cap$ `integrableExpSet Y Q` is LMLExplore's
-       `MGFDominatedAbove X P Y Q` (and on $(-\infty,0]$, `MGFDominatedBelow`); the Chernoff bounds
-       of Layer 1.2 hold under the conditional version along a filtration;
+       variable $Y$ on $\Lambda\cap$ `integrableExpSet Y Q` is LMLExplore's
+       `MGFDominatedOn X P Y Q Λ` (`mgfDominatedOn_iff_hasMGFBound`); the Chernoff bounds of
+       Layer 1.2 hold under the conditional version along a filtration;
      - $\psi$ the cumulant generating function of the statistic under a member of an exponential
        family on $[0,\infty)$ or $(-\infty,0]$ (the domination of $[0,1]$-valued variables by
        Bernoulli laws is the Bandits roadmap's Layer 1.4);
-     - if $X-\mu$ is conditionally σ²-sub-Gaussian, then $X$ is conditionally dominated above and
-       below by the member of mean $\mu$ of the Gaussian family of variance σ², so that the
+     - if $X-\mu$ is conditionally σ²-sub-Gaussian, then $X$ is conditionally dominated on
+       $\mathbb R$ by the member of mean $\mu$ of the Gaussian family of variance σ², so that the
        Gaussian-family inequalities below apply to σ²-sub-Gaussian rewards.
    - **Exponential supermartingales.** For a filtration $\mathcal F$, a process $(X_k)$ with $X_k$
      $\mathcal F_{k+1}$-measurable and with moment generating function conditionally bounded by

LMLRoadmaps/Identification/Suggested.lean

@@ -374,8 +374,8 @@ structure Kernel.HasCGFBound (X : Ω → ℝ) (ψ : ℝ → ℝ) (Λ : Set ℝ)
   mgf_le : ∀ᵐ ω' ∂ν, ∀ t ∈ Λ, mgf X (κ ω') t ≤ exp (ψ t)
 
 /-- The moment generating function of `X` under `P` is bounded by `exp ψ` on `Λ`. With `ψ` the
-cumulant generating function of `Y` under `Q` on `[0, ∞) ∩ integrableExpSet Y Q`, this is
-LMLExplore's `MGFDominatedAbove X P Y Q`. -/
+cumulant generating function of `Y` under `Q` on `Λ ∩ integrableExpSet Y Q`, this is
+LMLExplore's `MGFDominatedOn X P Y Q Λ`. -/
 structure HasCGFBound (X : Ω → ℝ) (ψ : ℝ → ℝ) (Λ : Set ℝ) (P : Measure Ω) : Prop where
   integrable_exp_mul : ∀ t ∈ Λ, Integrable (fun ω ↦ exp (t * X ω)) P
   mgf_le : ∀ t ∈ Λ, mgf X P t ≤ exp (ψ t)
@@ -407,7 +407,7 @@ theorem supermartingale_exp_sum_of_hasCondCGFBound [StandardBorelSpace Ω] {P :
   sorry
 
 /-- **Cramér–Chernoff bound with the rate function** (README Layer 1.2), at every level above
-the mean, for independent variables dominated above by `Y`. -/
+the mean, for independent variables dominated by `Y` on `[0, ∞)`. -/
 theorem measureReal_sum_ge_le_exp_of_le_rateFunction {P : Measure Ω} [IsProbabilityMeasure P]
     {Q : Measure Ω'} [IsProbabilityMeasure Q] {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} (hY : Integrable Y Q)
     (h_indep : iIndepFun X P)