From 8ae6d4f8ce3081537549c20e3db443577cb55e67 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 08:58:18 +0100 Subject: [PATCH 1/3] feat: the eventual regret of ucbF as the Gaussian instance of KL-UCB Co-Authored-By: Claude Code --- .../Bandits/AsymptoticallyOptimalUCB.lean | 48 +++---------------- LMLExplore/Bandits/KLUCB.lean | 45 ++++++++++++++++- 2 files changed, 50 insertions(+), 43 deletions(-) diff --git a/LMLExplore/Bandits/AsymptoticallyOptimalUCB.lean b/LMLExplore/Bandits/AsymptoticallyOptimalUCB.lean index 33d7c766..ce590324 100644 --- a/LMLExplore/Bandits/AsymptoticallyOptimalUCB.lean +++ b/LMLExplore/Bandits/AsymptoticallyOptimalUCB.lean @@ -9,7 +9,6 @@ public import LeanMachineLearning.Online.Bandit.Regret public import LMLExplore.Analysis.SpecialFunctions.Log.Basic public import LMLExplore.Bandits.Concentration public import LMLExplore.Bandits.IndexAlgorithm -public import LMLExplore.Bandits.Regret /-! # Asymptotically optimal UCB @@ -48,12 +47,12 @@ Lean round `n` uses `log f(n + 1)`. `1 + 5 σ² / ε² + 2 σ² (log f(n) + √(π log f(n)) + 1) / (Δ_a - ε)²` on the expected number of pulls of an arm `a` with gap `Δ_a`, for every `ε ∈ (0, Δ_a)`. * `ucbF_regret_le`: [LS, Theorem 8.1], the finite-time bound on the expected regret. -* `UCBF.integral_pullCount_eventually_le`: for an arm `a` with positive gap `Δ_a` and every - `c > 2 σ² / Δ_a²`, eventually `E[T_a(n)] ≤ c log n`, that is, - `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²`. -* `ucbF_regret_eventually_le`: [LS, (8.2)], the asymptotic part of [LS, Theorem 8.1]: for every - `c > ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, eventually `E[R_n] ≤ c log n`, that is, - `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`. + +The asymptotic part of [LS, Theorem 8.1], `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, +and its form `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²` for the number of pulls, are the Gaussian +instances of the asymptotic bounds of KL-UCB for exponential families, since `ucbF σ2` is KL-UCB +for the Gaussian family of variance `σ²`: they are `ucbF_regret_eventually_le` and +`UCBF.integral_pullCount_eventually_le` in `LMLExplore.Bandits.KLUCB`. ## Implementation notes @@ -64,10 +63,6 @@ sum, the overestimation of `a` by more than `Δ_a - ε`, is bounded by [LS, Lemm i.i.d. reward stream model, by `sum_measureReal_action_eq_and_pullCount_eq_zero_or_lt_empMean_add_sqrt_le`. -For the asymptotic bound, `ε` is chosen small enough that `2 σ² / (Δ_a - ε)² < c`. The bound of -`UCBF.integral_pullCount_le` divided by `log n` then tends to `2 σ² / (Δ_a - ε)²`, since -`log f(n) / log n → 1` (`Real.tendsto_log_one_add_mul_log_sq_div_log_atTop`). - ## References * [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020, @@ -265,37 +260,6 @@ theorem ucbF_regret_le exact le_ciInf fun ε ↦ mul_le_mul_of_nonneg_left (UCBF.integral_pullCount_le h hν hσ2 a ε.2.1 ε.2.2 n) gap_nonneg -/-- **Asymptotic number of pulls of asymptotically optimal UCB.** For σ²-sub-Gaussian rewards -with `σ² ≠ 0`, an arm `a` with positive gap `Δ_a`, and every `c > 2 σ² / Δ_a²`, the expected -number of pulls of `a` during the first `n` rounds is eventually at most `c log n`; that is, -`limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²`. -/ -theorem UCBF.integral_pullCount_eventually_le - (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P) - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (a : α) - (ha : 0 < gap ν a) {c : ℝ} (hc : 2 * σ2 / gap ν a ^ 2 < c) : - ∀ᶠ n : ℕ in atTop, P[fun ω ↦ (pullCount A a n ω : ℝ)] ≤ c * log n := - eventually_le_mul_log_of_forall_le_add_mul_add_sqrt_add_one - (L := fun n ↦ log (1 + n * log n ^ 2)) ha - (tendsto_log_one_add_mul_log_sq_div_log_atTop.comp tendsto_natCast_atTop_atTop) pi_pos.le - (fun ε hε ↦ ⟨1 + 5 * σ2 / ε ^ 2, fun n ↦ - (UCBF.integral_pullCount_le h hν hσ2 a hε.1 hε.2 n).trans_eq (by ring)⟩) hc - -/-- **[LS, (8.2)]**, the asymptotic part of [LS, Theorem 8.1]. For σ²-sub-Gaussian rewards with -`σ² ≠ 0` and every `c > ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, the expected regret of the asymptotically -optimal UCB algorithm at horizon `n` is eventually at most `c log n`; that is, -`limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`. -/ -theorem ucbF_regret_eventually_le [StandardBorelSpace α] - (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P) - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ} - (hc : ∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), 2 * σ2 / gap ν a < c) : - ∀ᶠ n : ℕ in atTop, P[regret ν A n] ≤ c * log n := by - refine integral_regret_eventually_le_of_forall_integral_pullCount_eventually_le - h.measurable_action (.of_forall fun n ↦ log_natCast_nonneg n) - (fun a ↦ 2 * σ2 / gap ν a ^ 2) - (fun a ha _ hc ↦ UCBF.integral_pullCount_eventually_le h hν hσ2 a ha hc) ?_ - refine (sum_congr rfl fun a ha ↦ ?_).trans_lt hc - field_simp [(mem_filter.mp ha).2.ne'] - end Regret end LMLExplore.Bandits diff --git a/LMLExplore/Bandits/KLUCB.lean b/LMLExplore/Bandits/KLUCB.lean index 5a8d1d63..55d06583 100644 --- a/LMLExplore/Bandits/KLUCB.lean +++ b/LMLExplore/Bandits/KLUCB.lean @@ -82,6 +82,10 @@ Lean round `n` uses `log f(n + 1)`. family of every arm with positive gap. * `klucbFam_gaussianReal_regret_eventually_le`: for `σ2_a`-sub-Gaussian rewards and the Gaussian families of variances `σ2_a`, `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ2_a / Δ_a`. +* `UCBF.integral_pullCount_eventually_le`, `ucbF_regret_eventually_le`: [LS, (8.2)], the + asymptotic part of [LS, Theorem 8.1], as the instance with a common variance `σ²`: for + σ²-sub-Gaussian rewards, `ucbF σ2` satisfies `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²` and + `limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`. * `KLUCB.integral_pullCount_le`: for rewards in `[0, 1]`, the bound `log f(n) / d(μ_a + ε₁, μ* - ε₂) + 1 / (2 ε₁²) + 2 / ε₂²` on the expected number of pulls of an arm `a` with gap `Δ_a`, for all `ε₁, ε₂ > 0` with `ε₁ + ε₂ < Δ_a`. @@ -141,7 +145,7 @@ this limit to its Exercise 10.2. ## References * [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020, - Chapter 10. + Chapters 8 and 10. * [GC11] A. Garivier and O. Cappé, *The KL-UCB algorithm for bounded stochastic bandits and beyond*, COLT 2011. * [CGMMS13] O. Cappé, A. Garivier, O.-A. Maillard, R. Munos and G. Stoltz, *Kullback–Leibler @@ -779,6 +783,45 @@ theorem klucbFam_gaussianReal_regret_eventually_le [StandardBorelSpace α] (m : (fun a _ ↦ mem_expFamilyMeans_gaussianReal _ (hσ2 a) _) ?_ exact (sum_gap_div_expFamilyDiv_gaussianReal m hσ2).trans_lt hc +/-- **Asymptotic number of pulls of asymptotically optimal UCB.** For σ²-sub-Gaussian rewards +with `σ² ≠ 0`, an arm `a` with positive gap `Δ_a`, and every `c > 2 σ² / Δ_a²`, the expected +number of pulls of `a` by `ucbF σ2` during the first `n` rounds is eventually at most `c log n`; +that is, `limsup_n E[T_a(n)] / log n ≤ 2 σ² / Δ_a²`. This is the Gaussian instance of +`KLUCBFam.integral_pullCount_eventually_le`, since `ucbF σ2` is KL-UCB for the Gaussian family of +variance `σ²` (`klucbFam_gaussianReal`) and `d(μ_a, μ*) = Δ_a² / (2 σ²)` for that family. -/ +theorem UCBF.integral_pullCount_eventually_le {σ2 : ℝ≥0} + (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P) + (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (a : α) + (ha : 0 < gap ν a) {c : ℝ} (hc : 2 * σ2 / gap ν a ^ 2 < c) : + ∀ᶠ n : ℕ in atTop, P[fun ω ↦ (pullCount A a n ω : ℝ)] ≤ c * log n := by + rw [← klucbFam_gaussianReal 0 hσ2] at h + -- every arm is dominated on `ℝ` by the member `𝒩(μ_b, σ2)` of the Gaussian family + have hdom (b : α) : MGFDominatedOn id (ν b) id ((gaussianReal 0 σ2).expFamily id + ((gaussianReal 0 σ2).natParam id (ν b)[id])) Set.univ := by + rw [expFamily_natParam_gaussianReal 0 hσ2] + exact (hν b).mgfDominatedOn_gaussianReal + have hgap : gap ν a = (ν (bestArm ν))[id] - (ν a)[id] := gap_eq_bestArm_sub + refine KLUCBFam.integral_pullCount_eventually_le (b := bestArm ν) h + (mem_expFamilyMeans_gaussianReal _ hσ2 _) + ((hdom a).mono (Set.subset_univ _)) (mem_expFamilyMeans_gaussianReal _ hσ2 _) + ((hdom _).mono (Set.subset_univ _)) (not_ae_eq_const_gaussianReal _ hσ2) (by linarith) + (mem_expFamilyMeans_gaussianReal _ hσ2 _) ?_ + rwa [expFamilyDiv_gaussianReal _ hσ2, ← neg_sub, neg_sq, ← hgap, inv_div] + +/-- **[LS, (8.2)]**, the asymptotic part of [LS, Theorem 8.1]. For σ²-sub-Gaussian rewards with +`σ² ≠ 0` and every `c > ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, the expected regret of the asymptotically +optimal UCB algorithm `ucbF σ2` at horizon `n` is eventually at most `c log n`; that is, +`limsup_n E[R_n] / log n ≤ ∑_{a : Δ_a > 0} 2 σ² / Δ_a`. This is the instance of +`klucbFam_gaussianReal_regret_eventually_le` with a common variance, since `ucbF σ2` is KL-UCB for +the Gaussian family of variance `σ²` (`klucbFam_gaussianReal`). -/ +theorem ucbF_regret_eventually_le [StandardBorelSpace α] {σ2 : ℝ≥0} + (h : IsAlgEnvSeq O A R (ucbF σ2) (Environment.bandit ν) P) + (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {c : ℝ} + (hc : ∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), 2 * σ2 / gap ν a < c) : + ∀ᶠ n : ℕ in atTop, P[regret ν A n] ≤ c * log n := by + rw [← klucbFam_gaussianReal 0 hσ2] at h + exact klucbFam_gaussianReal_regret_eventually_le (fun _ ↦ 0) h hν (fun _ ↦ hσ2) hc + end FamilyRegret end LMLExplore.Bandits From 7636fcbfd3baa17767e99f12c2a37fb84ce40df3 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 09:24:15 +0100 Subject: [PATCH 2/3] refactor: share the Gaussian MGF dominance and gap divergence in KL-UCB proofs Factor out HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal and expFamilyDiv_gaussianReal_eq_gap_sq, used by sum_gap_div_expFamilyDiv_gaussianReal, klucbFam_gaussianReal_regret_eventually_le and UCBF.integral_pullCount_eventually_le. Co-Authored-By: Claude Code --- LMLExplore/Bandits/KLUCB.lean | 37 +++++++++++++++++++++++------------ 1 file changed, 25 insertions(+), 12 deletions(-) diff --git a/LMLExplore/Bandits/KLUCB.lean b/LMLExplore/Bandits/KLUCB.lean index 55d06583..e4cde1df 100644 --- a/LMLExplore/Bandits/KLUCB.lean +++ b/LMLExplore/Bandits/KLUCB.lean @@ -745,6 +745,25 @@ theorem klucbFam_regret_eventually_le [StandardBorelSpace α] (by linarith [gap_eq_bestArm_sub (ν := ν) (a := a)]) (hμs a ha) hc) (by simpa only [div_eq_mul_inv] using hc) +omit [DecidableEq α] [MeasurableSingletonClass α] [IsMarkovKernel ν] in +/-- If `X - a` is `σ2`-sub-Gaussian with `σ2 ≠ 0`, then `X` is dominated on `ℝ` by the member of +mean `a` of the Gaussian family of variance `σ2` generated by any `𝒩(m, σ2)`. -/ +lemma _root_.ProbabilityTheory.HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal + {β : Type*} {mβ : MeasurableSpace β} {X : β → ℝ} {Q : Measure β} {a : ℝ} {σ2 : ℝ≥0} + (h : HasSubgaussianMGF (fun x ↦ X x - a) σ2 Q) (m : ℝ) (hσ2 : σ2 ≠ 0) : + MGFDominatedOn X Q id ((gaussianReal m σ2).expFamily id ((gaussianReal m σ2).natParam id a)) + Set.univ := by + rw [expFamily_natParam_gaussianReal m hσ2] + exact h.mgfDominatedOn_gaussianReal + +omit [DecidableEq α] [MeasurableSingletonClass α] [IsMarkovKernel ν] in +/-- For the Gaussian family of variance `σ2 ≠ 0`, the divergence from the mean of an arm `a` to the +best mean is `d(μ_a, μ*) = Δ_a² / (2 σ2)`. -/ +lemma expFamilyDiv_gaussianReal_eq_gap_sq (m : ℝ) {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) (a : α) : + (gaussianReal m σ2).expFamilyDiv id (ν a)[id] (ν (bestArm ν))[id] = + gap ν a ^ 2 / (2 * σ2) := by + rw [expFamilyDiv_gaussianReal _ hσ2, ← neg_sub, neg_sq, ← gap_eq_bestArm_sub] + omit [DecidableEq α] [MeasurableSingletonClass α] [IsMarkovKernel ν] in /-- For the Gaussian families of variances `σ2 a ≠ 0`, the constant `∑_{a : Δ_a > 0} Δ_a / d_{ρ a}(μ_a, μ*)` is `∑_{a : Δ_a > 0} 2 σ2_a / Δ_a`, since @@ -756,7 +775,7 @@ lemma sum_gap_div_expFamilyDiv_gaussianReal (m : α → ℝ) {σ2 : α → ℝ refine sum_congr rfl fun a ha ↦ ?_ have hga := (mem_filter.mp ha).2 have hσ2a : (σ2 a : ℝ) ≠ 0 := NNReal.coe_ne_zero.2 (hσ2 a) - rw [expFamilyDiv_gaussianReal _ (hσ2 a), ← neg_sub, neg_sq, ← gap_eq_bestArm_sub] + rw [expFamilyDiv_gaussianReal_eq_gap_sq _ (hσ2 a)] field_simp /-- **Asymptotic regret of KL-UCB for Gaussian families with known variances.** Let the rewards @@ -772,10 +791,7 @@ theorem klucbFam_gaussianReal_regret_eventually_le [StandardBorelSpace α] (m : {c : ℝ} (hc : ∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), 2 * σ2 a / gap ν a < c) : ∀ᶠ n : ℕ in atTop, P[regret ν A n] ≤ c * log n := by -- every arm is dominated on `ℝ` by the member `𝒩(μ_a, σ2 a)` of its family - have hdom (a : α) : MGFDominatedOn id (ν a) id ((gaussianReal (m a) (σ2 a)).expFamily id - ((gaussianReal (m a) (σ2 a)).natParam id (ν a)[id])) Set.univ := by - rw [expFamily_natParam_gaussianReal (m a) (hσ2 a)] - exact (hν a).mgfDominatedOn_gaussianReal + have hdom (a : α) := (hν a).mgfDominatedOn_expFamily_natParam_gaussianReal (m a) (hσ2 a) refine klucbFam_regret_eventually_le h (fun a _ ↦ mem_expFamilyMeans_gaussianReal _ (hσ2 a) _) (mem_expFamilyMeans_gaussianReal _ (hσ2 _) _) (fun a _ ↦ (hdom a).mono (Set.subset_univ _)) ((hdom _).mono (Set.subset_univ _)) @@ -796,17 +812,14 @@ theorem UCBF.integral_pullCount_eventually_le {σ2 : ℝ≥0} ∀ᶠ n : ℕ in atTop, P[fun ω ↦ (pullCount A a n ω : ℝ)] ≤ c * log n := by rw [← klucbFam_gaussianReal 0 hσ2] at h -- every arm is dominated on `ℝ` by the member `𝒩(μ_b, σ2)` of the Gaussian family - have hdom (b : α) : MGFDominatedOn id (ν b) id ((gaussianReal 0 σ2).expFamily id - ((gaussianReal 0 σ2).natParam id (ν b)[id])) Set.univ := by - rw [expFamily_natParam_gaussianReal 0 hσ2] - exact (hν b).mgfDominatedOn_gaussianReal - have hgap : gap ν a = (ν (bestArm ν))[id] - (ν a)[id] := gap_eq_bestArm_sub + have hdom (b : α) := (hν b).mgfDominatedOn_expFamily_natParam_gaussianReal 0 hσ2 refine KLUCBFam.integral_pullCount_eventually_le (b := bestArm ν) h (mem_expFamilyMeans_gaussianReal _ hσ2 _) ((hdom a).mono (Set.subset_univ _)) (mem_expFamilyMeans_gaussianReal _ hσ2 _) - ((hdom _).mono (Set.subset_univ _)) (not_ae_eq_const_gaussianReal _ hσ2) (by linarith) + ((hdom _).mono (Set.subset_univ _)) (not_ae_eq_const_gaussianReal _ hσ2) + (by linarith [gap_eq_bestArm_sub (ν := ν) (a := a)]) (mem_expFamilyMeans_gaussianReal _ hσ2 _) ?_ - rwa [expFamilyDiv_gaussianReal _ hσ2, ← neg_sub, neg_sq, ← hgap, inv_div] + rwa [expFamilyDiv_gaussianReal_eq_gap_sq _ hσ2, inv_div] /-- **[LS, (8.2)]**, the asymptotic part of [LS, Theorem 8.1]. For σ²-sub-Gaussian rewards with `σ² ≠ 0` and every `c > ∑_{a : Δ_a > 0} 2 σ² / Δ_a`, the expected regret of the asymptotically From 74c8676713956b249421443fdcc9c8ccb4c47af0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 09:58:45 +0100 Subject: [PATCH 3/3] refactor: move the Gaussian MGF dominance lemma to the Gaussian exponential family Co-Authored-By: Claude Code --- LMLExplore/Bandits/KLUCB.lean | 11 ----------- .../Distributions/ExponentialFamily/Gaussian.lean | 13 +++++++++++++ 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/LMLExplore/Bandits/KLUCB.lean b/LMLExplore/Bandits/KLUCB.lean index e4cde1df..5a68abce 100644 --- a/LMLExplore/Bandits/KLUCB.lean +++ b/LMLExplore/Bandits/KLUCB.lean @@ -745,17 +745,6 @@ theorem klucbFam_regret_eventually_le [StandardBorelSpace α] (by linarith [gap_eq_bestArm_sub (ν := ν) (a := a)]) (hμs a ha) hc) (by simpa only [div_eq_mul_inv] using hc) -omit [DecidableEq α] [MeasurableSingletonClass α] [IsMarkovKernel ν] in -/-- If `X - a` is `σ2`-sub-Gaussian with `σ2 ≠ 0`, then `X` is dominated on `ℝ` by the member of -mean `a` of the Gaussian family of variance `σ2` generated by any `𝒩(m, σ2)`. -/ -lemma _root_.ProbabilityTheory.HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal - {β : Type*} {mβ : MeasurableSpace β} {X : β → ℝ} {Q : Measure β} {a : ℝ} {σ2 : ℝ≥0} - (h : HasSubgaussianMGF (fun x ↦ X x - a) σ2 Q) (m : ℝ) (hσ2 : σ2 ≠ 0) : - MGFDominatedOn X Q id ((gaussianReal m σ2).expFamily id ((gaussianReal m σ2).natParam id a)) - Set.univ := by - rw [expFamily_natParam_gaussianReal m hσ2] - exact h.mgfDominatedOn_gaussianReal - omit [DecidableEq α] [MeasurableSingletonClass α] [IsMarkovKernel ν] in /-- For the Gaussian family of variance `σ2 ≠ 0`, the divergence from the mean of an arm `a` to the best mean is `d(μ_a, μ*) = Δ_a² / (2 σ2)`. -/ diff --git a/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean b/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean index fa119c5a..c9205df0 100644 --- a/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean +++ b/LMLExplore/Probability/Distributions/ExponentialFamily/Gaussian.lean @@ -10,6 +10,7 @@ public import LMLExplore.Probability.Distributions.ExponentialFamily.Invariance public import LMLExplore.Probability.Distributions.ExponentialFamily.Posterior.Basic public import LMLExplore.Probability.Distributions.ExponentialFamily.UpperConfidence public import LMLExplore.Probability.Distributions.Gaussian.Real +public import LMLExplore.Probability.Moments.MGF.Bound public import TauCeti.Probability.Distributions.Tilted /-! @@ -74,6 +75,8 @@ Fixed variance, statistic `id`: * `LMLExplore.natParam_gaussianReal`: for `v ≠ 0`, the natural parameter of the mean `μ` is `(μ - m) / v`. * `LMLExplore.expFamily_natParam_gaussianReal`: for `v ≠ 0`, the member of mean `μ` is `𝒩(μ, v)`. +* `ProbabilityTheory.HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal`: if `X - a` + is `v`-sub-Gaussian with `v ≠ 0`, then `X` is MGF-dominated on `ℝ` by the member of mean `a`. * `LMLExplore.image_expFamily_gaussianReal`: for `v ≠ 0`, the members of the family are the Gaussian laws of variance `v`. * `LMLExplore.expFamilyDiv_gaussianReal`: for `v ≠ 0`, the divergence of the family is @@ -208,6 +211,16 @@ theorem expFamily_natParam_gaussianReal (m : ℝ) (hv : v ≠ 0) (μ : ℝ) : field_simp ring +/-- If `X - a` is `σ2`-sub-Gaussian with `σ2 ≠ 0`, then `X` is dominated on `ℝ` by the member of +mean `a` of the Gaussian family of variance `σ2` generated by any `𝒩(m, σ2)`. -/ +lemma _root_.ProbabilityTheory.HasSubgaussianMGF.mgfDominatedOn_expFamily_natParam_gaussianReal + {β : Type*} {mβ : MeasurableSpace β} {X : β → ℝ} {Q : Measure β} {a : ℝ} {σ2 : ℝ≥0} + (h : HasSubgaussianMGF (fun x ↦ X x - a) σ2 Q) (m : ℝ) (hσ2 : σ2 ≠ 0) : + MGFDominatedOn X Q id ((gaussianReal m σ2).expFamily id ((gaussianReal m σ2).natParam id a)) + Set.univ := by + rw [expFamily_natParam_gaussianReal m hσ2] + exact h.mgfDominatedOn_gaussianReal + /-- For `v ≠ 0`, the members of the exponential family of `𝒩(m, v)` are the Gaussian laws `𝒩(μ, v)` of variance `v`, for every mean `μ`. -/ theorem image_expFamily_gaussianReal (m : ℝ) (hv : v ≠ 0) :