refactor: one MGF domination predicate on a set of parameters

LMLExplore/Identification/CTracking.lean

@@ -239,17 +239,15 @@ variable {Ω 𝓧 : Type*} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 
 /-- **Concentration of the empirical means under C-tracking** [GK16, Lemma 19], in the form used
 in the proof of [GK16, Theorem 14]. In a run of C-tracking against the stochastic bandit
 `Environment.bandit ν`, with targets that are allocations, let the rewards of each arm `a` be
-dominated above and below by the member of mean `μ a` of the exponential family of `ρ a` and `T a`,
+dominated on `Set.univ` by the member of mean `μ a` of the exponential family of `ρ a` and `T a`,
 and let `l a < μ a < u a` be means of the family. If the rounds `t₀ T` satisfy
 `√(t₀ T) / log T → ∞`, then the probabilities that the empirical mean of some arm `a` is outside
 `(l a, u a)` at some round `t ≥ t₀ T` have a finite sum over `T`. -/
 theorem tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top (hw0 : ∀ n h a, 0 ≤ w n h a)
     (hw1 : ∀ n h, ∑ a, w n h a = 1)
     (h : IsAlgEnvSeq O A R (cTracking w hw) (Environment.bandit ν) P)
-    (hν_above : ∀ a, MGFDominatedAbove id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
-    (hν_below : ∀ a, MGFDominatedBelow id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
+    (hν : ∀ a, MGFDominatedOn id (ν a) (T a)
+      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ)
     (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) (hl : ∀ a, l a ∈ (ρ a).expFamilyMeans (T a))
     (hu : ∀ a, u a ∈ (ρ a).expFamilyMeans (T a)) (hlμ : ∀ a, l a < μ a) (hμu : ∀ a, μ a < u a)
     {t₀ : ℕ → ℕ} (ht₀ : Tendsto (fun T : ℕ ↦ √(t₀ T : ℝ) / Real.log T) atTop atTop) :
@@ -263,7 +261,7 @@ theorem tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top (hw0 : ∀ n h a, 0 ≤
     linarith [hω (t₀ T) a]
   -- Forced exploration is sufficient exploration on the sure event.
   simpa only [Set.univ_inter] using Identification.tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top
-    h hν_above hν_below hμ hl hu hlμ hμu (G := fun _ ↦ Set.univ)
+    h hν hμ hl hu hlμ hμu (G := fun _ ↦ Set.univ)
     (fun T ↦ (h_forced T).mono fun _ hω _ ↦ hω) (Real.tendsto_natCeil_sub_div_log _ ht₀)
 
 end CTracking

LMLExplore/Identification/DTracking.lean

@@ -222,17 +222,15 @@ variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {ν : Kernel α ℝ} [IsM
 
 /-- **Concentration of the empirical means under D-tracking** [GK16, Lemma 19], in the form used
 in the proof of [GK16, Theorem 14]. In a run of D-tracking against the stochastic bandit
-`Environment.bandit ν`, let the rewards of each arm `a` be dominated above and below by the member
+`Environment.bandit ν`, let the rewards of each arm `a` be dominated on `Set.univ` by the member
 of mean `μ a` of the exponential family of `ρ a` and `T a`, and let `l a < μ a < u a` be means of
 the family. If the rounds `t₀ T` satisfy `√(t₀ T) / log T → ∞` (for instance `t₀ T = ⌈T ^ (1 / 4)⌉₊`
 as in [GK16]), then the probabilities that the empirical mean of some arm `a` is outside
 `(l a, u a)` at some round `t ≥ t₀ T` have a finite sum over `T`. -/
 theorem tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top [IsProbabilityMeasure P]
     (h : IsAlgEnvSeq O A R (dTracking w hw) (Environment.bandit ν) P)
-    (hν_above : ∀ a, MGFDominatedAbove id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
-    (hν_below : ∀ a, MGFDominatedBelow id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
+    (hν : ∀ a, MGFDominatedOn id (ν a) (T a)
+      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ)
     (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) (hl : ∀ a, l a ∈ (ρ a).expFamilyMeans (T a))
     (hu : ∀ a, u a ∈ (ρ a).expFamilyMeans (T a)) (hlμ : ∀ a, l a < μ a) (hμu : ∀ a, μ a < u a)
     {t₀ : ℕ → ℕ} (ht₀ : Tendsto (fun T : ℕ ↦ √(t₀ T : ℝ) / log T) atTop atTop) :
@@ -244,7 +242,7 @@ theorem tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top [IsProbabilityMeasure P
     linarith [hω (t₀ T) a]
   -- Forced exploration is sufficient exploration on the sure event.
   simpa only [Set.univ_inter] using Identification.tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top
-    h hν_above hν_below hμ hl hu hlμ hμu (G := fun _ ↦ Set.univ)
+    h hν hμ hl hu hlμ hμu (G := fun _ ↦ Set.univ)
     (fun T ↦ (h_forced T).mono fun _ hω _ ↦ hω) (Real.tendsto_natCeil_sub_div_log _ ht₀)
 
 end DTracking

LMLExplore/Identification/ForcedExploration.lean

@@ -24,7 +24,7 @@ events `E_T` fail with probabilities that sum to a finite value, as the generic
 exploration is an event rather than a property of every run, so that the statements apply to rules
 that explore only with high probability; forced exploration is the case `G = Set.univ`.
 
-The rewards of each arm `a` are dominated, above and below, by the member of mean `μ a` of an
+The rewards of each arm `a` are dominated on `Set.univ` by the member of mean `μ a` of an
 exponential family `(ρ a, T a)` with divergence `d_a` (for instance their law is that member). For
 one arm, the probability that, at some round, it has at least `m` pulls and an empirical mean
 outside `(l a, u a)` is bounded by the Cramér–Chernoff bound and a union bound over the numbers of
@@ -75,17 +75,15 @@ variable [Fintype α] {ρ : α → Measure 𝓧} {T : α → 𝓧 → ℝ} {μ l
 
 /-- **Concentration of the empirical means under sufficient exploration** [GK16, Lemma 19]. In a run
 of any algorithm against the stochastic bandit `Environment.bandit ν`, let the rewards of each arm
-`a` be dominated above and below by the member of mean `μ a` of the exponential family of `ρ a` and
+`a` be dominated on `Set.univ` by the member of mean `μ a` of the exponential family of `ρ a` and
 `T a`, with divergence `d_a`, and let `l a < μ a < u a` be means of the family. If almost surely on
 an event `G` every arm has at least `m` pulls after `t₀` rounds, then the probability of `G` and of
 the empirical mean of some arm `a` being outside `(l a, u a)` at some round `t ≥ t₀` is at most
 `∑ a, (exp (-m d_a(u a, μ a)) / (1 - exp (-d_a(u a, μ a))) +
   exp (-m d_a(l a, μ a)) / (1 - exp (-d_a(l a, μ a))))`. The event `G` need not be measurable. -/
 theorem measure_exists_ge_empMean_notMem_Ioo_le (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
-    (hν_above : ∀ a, MGFDominatedAbove id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
-    (hν_below : ∀ a, MGFDominatedBelow id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
+    (hν : ∀ a, MGFDominatedOn id (ν a) (T a)
+      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ)
     (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) (hl : ∀ a, l a ∈ (ρ a).expFamilyMeans (T a))
     (hu : ∀ a, u a ∈ (ρ a).expFamilyMeans (T a)) (hlμ : ∀ a, l a < μ a) (hμu : ∀ a, μ a < u a)
     {G : Set Ω} {t₀ m : ℕ} (h_forced : ∀ᵐ ω ∂P, ω ∈ G → ∀ a, m ≤ pullCount A a t₀ ω) :
@@ -106,7 +104,7 @@ theorem measure_exists_ge_empMean_notMem_Ioo_le (h : IsAlgEnvSeq O A R alg (Envi
       (exp_neg_mul_div_one_sub_exp_neg_nonneg (Measure.expFamilyDiv_nonneg (hu a) (hμ a)) _)
       (exp_neg_mul_div_one_sub_exp_neg_nonneg (Measure.expFamilyDiv_nonneg (hl a) (hμ a)) _)]
     exact Finset.sum_le_sum fun a _ ↦
-      measure_exists_le_pullCount_and_empMean_notMem_Ioo_le h (hν_above a) (hν_below a)
+      measure_exists_le_pullCount_and_empMean_notMem_Ioo_le h (hν a)
         (hμ a) (hl a) (hu a) (hlμ a) (hμu a) m
 
 /-- **Concentration of the empirical means under exploration in a window** [GK16, Lemma 19]. Under
@@ -117,10 +115,8 @@ event `G` every arm has at least `g t` pulls at every round `t ∈ [t₀, t₁]`
 Since the pull counts are nondecreasing, only the first round of the window enters the bound. -/
 theorem measure_exists_mem_Icc_empMean_notMem_Ioo_le
     (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
-    (hν_above : ∀ a, MGFDominatedAbove id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
-    (hν_below : ∀ a, MGFDominatedBelow id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
+    (hν : ∀ a, MGFDominatedOn id (ν a) (T a)
+      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ)
     (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) (hl : ∀ a, l a ∈ (ρ a).expFamilyMeans (T a))
     (hu : ∀ a, u a ∈ (ρ a).expFamilyMeans (T a)) (hlμ : ∀ a, l a < μ a) (hμu : ∀ a, μ a < u a)
     {G : Set Ω} {g : ℕ → ℕ} {t₀ t₁ : ℕ}
@@ -136,7 +132,7 @@ theorem measure_exists_mem_Icc_empMean_notMem_Ioo_le
   calc P (G ∩ E)
   _ ≤ P ((G ∩ E) ∩ {ω | ∃ t ≥ t₀, ∃ a, empMean A R a t ω ∉ Set.Ioo (l a) (u a)}) :=
     measure_mono fun ω hω ↦ ⟨hω, by obtain ⟨t, ht, a, ha⟩ := hω.2; exact ⟨t, ht.1, a, ha⟩⟩
-  _ ≤ _ := measure_exists_ge_empMean_notMem_Ioo_le h hν_above hν_below hμ hl hu hlμ hμu
+  _ ≤ _ := measure_exists_ge_empMean_notMem_Ioo_le h hν hμ hl hu hlμ hμu
     (h_forced.mono fun ω hω ⟨hG, t, ht, _⟩ ↦ hω hG t₀ ⟨le_rfl, ht.1.trans ht.2⟩)
 
 omit [Fintype α] in
@@ -148,10 +144,8 @@ arm has at least `m T` pulls after `t₀ T` rounds, with `m T / log T → ∞`,
 `t ≥ t₀ T` have a finite sum over `T`. -/
 theorem tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top [Finite α]
     (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
-    (hν_above : ∀ a, MGFDominatedAbove id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
-    (hν_below : ∀ a, MGFDominatedBelow id (ν a) (T a)
-      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))))
+    (hν : ∀ a, MGFDominatedOn id (ν a) (T a)
+      ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ)
     (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) (hl : ∀ a, l a ∈ (ρ a).expFamilyMeans (T a))
     (hu : ∀ a, u a ∈ (ρ a).expFamilyMeans (T a)) (hlμ : ∀ a, l a < μ a) (hμu : ∀ a, μ a < u a)
     {G : ℕ → Set Ω} {t₀ m : ℕ → ℕ}
@@ -166,7 +160,7 @@ theorem tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top [Finite α]
     summable_exp_neg_of_tendsto_div_log <| (hm.atTop_mul_const hd).congr fun T ↦
       div_mul_eq_mul_div _ _ _
   refine ne_top_of_le_ne_top ?_ (tsum_le_tsum fun T ↦
-    measure_exists_ge_empMean_notMem_Ioo_le h hν_above hν_below hμ hl hu hlμ hμu (h_forced T))
+    measure_exists_ge_empMean_notMem_Ioo_le h hν hμ hl hu hlμ hμu (h_forced T))
   rw [← ENNReal.ofReal_tsum_of_nonneg (fun T ↦ sum_nonneg fun a _ ↦ add_nonneg
       (exp_neg_mul_div_one_sub_exp_neg_nonneg (hdu a).le _)
       (exp_neg_mul_div_one_sub_exp_neg_nonneg (hdl a).le _))

LMLExplore/Identification/GaussianThreshold.lean

@@ -91,27 +91,16 @@ open scoped ENNReal NNReal
 
 namespace LMLExplore.Identification.IdentTask
 
-/-- For Gaussian arms with a common variance `σ2 ≠ 0`, the arm `a` of the model `θ` is dominated
-above, in moment generating function, by the member of mean `θ a` of the exponential family of
-`𝒩(0, σ2)` with the identity statistic: both have the law `𝒩(θ a, σ2)`. -/
-private lemma mgfDominatedAbove_gaussianBandit {α ℐ : Type*} {mα : MeasurableSpace α} [Countable α]
+/-- For Gaussian arms with a common variance `σ2 ≠ 0`, the arm `a` of the model `θ` is dominated,
+in moment generating function and on every parameter, by the member of mean `θ a` of the
+exponential family of `𝒩(0, σ2)` with the identity statistic: both have the law `𝒩(θ a, σ2)`. -/
+private lemma mgfDominatedOn_gaussianBandit {α ℐ : Type*} {mα : MeasurableSpace α} [Countable α]
     [MeasurableSingletonClass α] {task : IdentTask α (α → ℝ) ℐ ℝ} {σ2 : ℝ≥0}
     (hνt : task.ν = (Bandits.gaussianBandit · σ2)) (hσ2 : σ2 ≠ 0) (θ : α → ℝ) (a : α) :
-    MGFDominatedAbove id (task.ν θ a) id
-      ((gaussianReal 0 σ2).expFamily id ((gaussianReal 0 σ2).natParam id (θ a))) := by
+    MGFDominatedOn id (task.ν θ a) id
+      ((gaussianReal 0 σ2).expFamily id ((gaussianReal 0 σ2).natParam id (θ a))) Set.univ := by
   rw [hνt, expFamily_natParam_gaussianReal 0 hσ2, Bandits.gaussianBandit_apply]
-  exact (IdentDistrib.refl aemeasurable_id).mgfDominatedAbove
-
-/-- For Gaussian arms with a common variance `σ2 ≠ 0`, the arm `a` of the model `θ` is dominated
-below, in moment generating function, by the member of mean `θ a` of the exponential family of
-`𝒩(0, σ2)` with the identity statistic: both have the law `𝒩(θ a, σ2)`. -/
-private lemma mgfDominatedBelow_gaussianBandit {α ℐ : Type*} {mα : MeasurableSpace α} [Countable α]
-    [MeasurableSingletonClass α] {task : IdentTask α (α → ℝ) ℐ ℝ} {σ2 : ℝ≥0}
-    (hνt : task.ν = (Bandits.gaussianBandit · σ2)) (hσ2 : σ2 ≠ 0) (θ : α → ℝ) (a : α) :
-    MGFDominatedBelow id (task.ν θ a) id
-      ((gaussianReal 0 σ2).expFamily id ((gaussianReal 0 σ2).natParam id (θ a))) := by
-  rw [hνt, expFamily_natParam_gaussianReal 0 hσ2, Bandits.gaussianBandit_apply]
-  exact (IdentDistrib.refl aemeasurable_id).mgfDominatedBelow
+  exact (IdentDistrib.refl aemeasurable_id).mgfDominatedOn
 
 variable {α ℐ : Type*} [Fintype α] [DecidableEq α] {mα : MeasurableSpace α}
   [MeasurableSingletonClass α] {task : IdentTask α (α → ℝ) ℐ ℝ} {σ2 : ℝ≥0}
@@ -268,7 +257,7 @@ theorem isDeltaPAC_trackAndStop_unionBoundThreshold_of_mem_optAlloc [MeasurableS
     (fun θ hθ ↦ hcorrect θ hθ ▸ measurableSet_singleton _) fun θ hθ ↦
     stopsAS_trackAndStop_unionBoundThreshold (fun _ ↦ not_ae_eq_const_gaussianReal 0 hσ2)
       (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (mgfDominatedAbove_gaussianBandit hνt hσ2 θ) (mgfDominatedBelow_gaussianBandit hνt hσ2 θ)
+      (mgfDominatedOn_gaussianBandit hνt hσ2 θ)
       (hcorrect θ hθ) (hw_opt θ hθ) (hw_cont θ hθ) (hrec_eq θ hθ) (h_lsc θ hθ) (h_charTime θ hθ)
       hδ hδ1
 
@@ -298,7 +287,7 @@ theorem tendsto_expectedStoppingTime_trackAndStop_unionBoundThreshold_div_log
       hw_cont hrec_eq h_lsc h_charTime hδ.1 hδ.2).isDeltaCorrect
   · exact eventually_expectedStoppingTime_trackAndStop_unionBoundThreshold_le
       (fun _ ↦ not_ae_eq_const_gaussianReal 0 hσ2) (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (mgfDominatedAbove_gaussianBandit hνt hσ2 μ) (mgfDominatedBelow_gaussianBandit hνt hσ2 μ)
+      (mgfDominatedOn_gaussianBandit hνt hσ2 μ)
       (hcorrect μ hμ) (hw_opt μ hμ) (hw_cont μ hμ) (hrec_eq μ hμ) (h_lsc μ hμ) hc
 
 end LMLExplore.Identification.IdentTask
@@ -338,9 +327,8 @@ theorem isDeltaPAC_cTrackAndStop_unionBoundThreshold_of_mem_optAlloc [Measurable
       hrec (hstop δ)) δ := by
   have h_stops (θ : α → ℝ) (hθ : θ ∈ task.M) := stopsAS_cTrackAndStop_unionBoundThreshold
     (hw := hw) (hrec := hrec) (hstop := hstop) (fun _ ↦ not_ae_eq_const_gaussianReal 0 hσ2)
-    (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _) (mgfDominatedAbove_gaussianBandit hνt hσ2 θ)
-    (mgfDominatedBelow_gaussianBandit hνt hσ2 θ) (hcorrect θ hθ) hw_mem (hw_opt θ hθ)
-    (hrec_eq θ hθ) (h_cont θ hθ) (h_charTime θ hθ) hδ hδ1
+    (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _) (mgfDominatedOn_gaussianBandit hνt hσ2 θ)
+    (hcorrect θ hθ) hw_mem (hw_opt θ hθ) (hrec_eq θ hθ) (h_cont θ hθ) (h_charTime θ hθ) hδ hδ1
   simp only [cTrackAndStop_def] at h_stops ⊢
   exact isDeltaPAC_glrt_unionBoundThreshold _ _ hνt hσ2 hδ hδ1 (hstop δ)
     (fun θ hθ ↦ hcorrect θ hθ ▸ measurableSet_singleton _) h_stops
@@ -372,7 +360,7 @@ theorem tendsto_expectedStoppingTime_cTrackAndStop_unionBoundThreshold_div_log
       hw_opt hrec_eq h_cont h_charTime hδ.1 hδ.2).isDeltaCorrect
   · exact eventually_expectedStoppingTime_cTrackAndStop_unionBoundThreshold_le
       (fun _ ↦ not_ae_eq_const_gaussianReal 0 hσ2) (fun _ ↦ mem_expFamilyMeans_gaussianReal 0 hσ2 _)
-      (mgfDominatedAbove_gaussianBandit hνt hσ2 μ) (mgfDominatedBelow_gaussianBandit hνt hσ2 μ)
+      (mgfDominatedOn_gaussianBandit hνt hσ2 μ)
       (hcorrect μ hμ) hw_mem (hw_opt μ hμ) (hrec_eq μ hμ) (h_cont μ hμ) hc
 
 end LMLExplore.Identification.IdentTask