From 26c94a020b6448f2c714b0d69f0023ab49c38a41 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 6 Nov 2026 07:27:32 +0100 Subject: [PATCH 1/2] refactor: one MGF domination predicate on a set of parameters MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit MGFDominatedAbove and MGFDominatedBelow become MGFDominatedOn X P Y Q Λ, domination at every t ∈ Λ: the upper tail uses Set.Ici 0, the lower tail Set.Iic 0, two-sided statements Set.univ. The pairs of lemmas merge (neg, trans, IdentDistrib, the independent sums, the bridge to HasMGFBound), the sums no longer need a sign condition, and the two-sided consumers take one hypothesis hν instead of hν_above and hν_below. Co-Authored-By: Claude Opus 5.5 --- LMLExplore/Identification/CTracking.lean | 10 +- LMLExplore/Identification/DTracking.lean | 10 +- .../Identification/ForcedExploration.lean | 28 +-- .../Identification/GaussianThreshold.lean | 36 +-- LMLExplore/Identification/TrackAndStop.lean | 72 +++--- .../ExponentialFamily/Chernoff.lean | 46 ++-- .../Probability/Moments/KLChernoff.lean | 45 ++-- LMLExplore/Probability/Moments/MGF/Bound.lean | 29 +-- .../Probability/Moments/MGF/Dominated.lean | 228 ++++++------------ .../ExpFamilyDeviation.lean | 36 +-- 10 files changed, 213 insertions(+), 327 deletions(-) diff --git a/LMLExplore/Identification/CTracking.lean b/LMLExplore/Identification/CTracking.lean index f5f3bd4d..97c615c7 100644 --- a/LMLExplore/Identification/CTracking.lean +++ b/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 diff --git a/LMLExplore/Identification/DTracking.lean b/LMLExplore/Identification/DTracking.lean index 6f07c53b..149bdb67 100644 --- a/LMLExplore/Identification/DTracking.lean +++ b/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 diff --git a/LMLExplore/Identification/ForcedExploration.lean b/LMLExplore/Identification/ForcedExploration.lean index 206f94fb..1af6b447 100644 --- a/LMLExplore/Identification/ForcedExploration.lean +++ b/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 _)) diff --git a/LMLExplore/Identification/GaussianThreshold.lean b/LMLExplore/Identification/GaussianThreshold.lean index de12d1ca..a3c121b3 100644 --- a/LMLExplore/Identification/GaussianThreshold.lean +++ b/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 diff --git a/LMLExplore/Identification/TrackAndStop.lean b/LMLExplore/Identification/TrackAndStop.lean index 6c16a0cb..82c456d1 100644 --- a/LMLExplore/Identification/TrackAndStop.lean +++ b/LMLExplore/Identification/TrackAndStop.lean @@ -373,7 +373,7 @@ private lemma mul_le_glr_plugInCost {Ω : Type*} {O : ℕ → Ω → Unit} {A : exact mul_le_mul_right (hU _ hU' q hq hq_dist).le _ /-- **Sample complexity of Track-and-Stop** [GK16, Theorem 14]. Let the rewards of each arm `a` of -the model `μ` be dominated above and below by the member of mean `μ a` of a nondegenerate +the model `μ` be dominated on `Set.univ` by the member of mean `μ a` of a nondegenerate exponential family `(ρ a, T a)`. Let the target map `w` be continuous at `μ` with `w(μ)` a probability vector, let the recommendation be `i` near `μ`, and let `(μ', w') ↦ D(μ', w', ¬i)` be lower semicontinuous at `(μ, w(μ))` on the allocations of the simplex. Then for thresholds @@ -383,10 +383,8 @@ means as estimator satisfies `𝔼[τ_δ] ≤ c log (1 / δ)` for all small enou bound for `r(t) = O(t ^ α)` has a factor `α ∈ [1, e / 2]`. -/ theorem eventually_expectedStoppingTime_trackAndStop_le (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hw_mem : w μ ∈ simplex α) (hw_cont : ContinuousAt w μ) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) (h_lsc : LowerSemicontinuousWithinAt (fun q : (α → ℝ) × (α → ℝ) ↦ task.altCost q.1 q.2 i) (Set.univ ×ˢ simplex α) (μ, w μ)) @@ -436,7 +434,7 @@ theorem eventually_expectedStoppingTime_trackAndStop_le (hT : ∀ a c, ¬ T a = pullCount IT.action (IT.action k ω) k ω)} have hE_sum : ∑' T, P (E T)ᶜ ≠ ∞ := by refine ne_top_of_le_ne_top (DTracking.tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top hseq - hν_above hν_below hμ (fun a ↦ hlW.2.2.2 a) (fun a ↦ huW.2.2.2 a) hlμ hμu + hν hμ (fun a ↦ hlW.2.2.2 a) (fun a ↦ huW.2.2.2 a) hlμ hμu tendsto_sqrt_roundsAfter_div_log) (tsum_le_tsum fun T ↦ measure_mono_ae ?_) filter_upwards [DTracking.pullCount_action_le_of_lt hseq, @@ -475,7 +473,7 @@ theorem eventually_expectedStoppingTime_trackAndStop_le (hT : ∀ a c, ¬ T a = /-- **Sample complexity of Track-and-Stop at the characteristic time** [GK16, Theorem 14], the upper bound `𝔼[τ_δ] ≤ c log (1 / δ)` with `c > T*(μ)`. Let the rewards of each arm `a` -of the model `μ` be dominated above and below by the member of mean `μ a` of a nondegenerate +of the model `μ` be dominated on `Set.univ` by the member of mean `μ a` of a nondegenerate exponential family `(ρ a, T a)`, let `i` be the single correct answer of `μ`, let the target map `w` be continuous at `μ` with `w(μ)` an optimal allocation `w*(μ, ¬i)`, let the recommendation be `i` near `μ`, and let `(μ', w') ↦ D(μ', w', ¬i)` be lower semicontinuous at `(μ, w(μ))` on the @@ -489,10 +487,8 @@ union-bound thresholds `K log (2 n (n + 1)) + x_δ` are `δ`-correct, and asympt `Identification/GaussianThreshold.lean`. -/ theorem eventually_expectedStoppingTime_trackAndStop_le_of_charTime_lt (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hcorrect : task.correct μ = {i}) (hw_opt : w μ ∈ task.optAlloc μ i) (hw_cont : ContinuousAt w μ) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) (h_lsc : LowerSemicontinuousWithinAt (fun q : (α → ℝ) × (α → ℝ) ↦ task.altCost q.1 q.2 i) @@ -503,7 +499,7 @@ theorem eventually_expectedStoppingTime_trackAndStop_le_of_charTime_lt (Environment.bandit (task.ν μ)) ≤ c * ENNReal.ofReal (log (1 / δ)) := by -- At an optimal allocation, `D(μ, w(μ), ¬i)⁻¹ = D(μ, ¬i)⁻¹ = T*(μ)`. rw [task.charTime_eq_inv_answerValue hcorrect, ← (task.mem_optAlloc_iff.1 hw_opt).2] at hc - exact task.eventually_expectedStoppingTime_trackAndStop_le hT hμ hν_above hν_below + exact task.eventually_expectedStoppingTime_trackAndStop_le hT hμ hν (task.mem_optAlloc_iff.1 hw_opt).1 hw_cont hrec_eq h_lsc hc hr hβ end LMLExplore.Identification.IdentTask @@ -533,10 +529,8 @@ on the model `μ`, Track-and-Stop with the thresholds `K log (2 n (n + 1)) + x_ `δ`-correct (`IdentTask.isDeltaPAC_trackAndStop_unionBoundThreshold`). -/ theorem eventually_expectedStoppingTime_trackAndStop_unionBoundThreshold_le (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hcorrect : task.correct μ = {i}) (hw_opt : w μ ∈ task.optAlloc μ i) (hw_cont : ContinuousAt w μ) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) (h_lsc : LowerSemicontinuousWithinAt (fun q : (α → ℝ) × (α → ℝ) ↦ task.altCost q.1 q.2 i) @@ -549,7 +543,7 @@ theorem eventually_expectedStoppingTime_trackAndStop_unionBoundThreshold_le -- At the confidence level `δ ^ (1 / s)`, the thresholds are at most `log (r n / δ)` with -- `r n = (2 n (n + 1)) ^ K`. exact task.eventually_expectedStoppingTime_trackAndStop_le_of_charTime_lt (hw := hw) - (hrec := hrec) (hstop := fun δ' ↦ hstop (δ' ^ s⁻¹)) hT hμ hν_above hν_below hcorrect hw_opt + (hrec := hrec) (hstop := fun δ' ↦ hstop (δ' ^ s⁻¹)) hT hμ hν hcorrect hw_opt hw_cont hrec_eq h_lsc hc' (isBigO_two_mul_mul_add_one_pow _) ((eventually_unionBoundThreshold_rpow_inv_le _ hs).mono fun _ h n hn _ ↦ h n hn) @@ -559,10 +553,8 @@ theorem eventually_expectedStoppingTime_trackAndStop_unionBoundThreshold_le `IdentTask.eventually_expectedStoppingTime_trackAndStop_unionBoundThreshold_le`. -/ theorem stopsAS_trackAndStop_unionBoundThreshold (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hcorrect : task.correct μ = {i}) (hw_opt : w μ ∈ task.optAlloc μ i) (hw_cont : ContinuousAt w μ) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) (h_lsc : LowerSemicontinuousWithinAt (fun q : (α → ℝ) × (α → ℝ) ↦ task.altCost q.1 q.2 i) @@ -575,7 +567,7 @@ theorem stopsAS_trackAndStop_unionBoundThreshold rw [ENNReal.coe_toNNReal h_charTime] exact ENNReal.lt_add_right h_charTime one_ne_zero have h := eventually_expectedStoppingTime_trackAndStop_unionBoundThreshold_le (hw := hw) - (hrec := hrec) (hstop := hstop) hT hμ hν_above hν_below hcorrect hw_opt hw_cont hrec_eq h_lsc hc + (hrec := hrec) (hstop := hstop) hT hμ hν hcorrect hw_opt hw_cont hrec_eq h_lsc hc simp only [trackAndStop_def] at h ⊢ exact stopsAS_glrt_unionBoundThreshold (h.mono fun _ hδ' ↦ ne_top_of_le_ne_top (ENNReal.mul_ne_top ENNReal.coe_ne_top ENNReal.ofReal_ne_top) hδ').frequently hδ hδ1 @@ -665,7 +657,7 @@ variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {ρ : α → Measure 𝓧 {r : ℕ → ℝ} {p : ℝ} {n₀ : ℕ} /-- **Sample complexity of Track-and-Stop with C-tracking** [DK19, Lemma 6 and Theorem 7]. Let the -rewards of each arm `a` of the model `μ` be dominated above and below by the member of mean `μ a` +rewards of each arm `a` of the model `μ` be dominated on `Set.univ` by the member of mean `μ a` of a nondegenerate exponential family `(ρ a, T a)`. Let the targets `w` be allocations that converge at `μ` to a convex compact set `C` (they eventually lie in every neighbourhood of `C`), let the recommendation be `i` near `μ`, and let `(μ', w') ↦ D(μ', w', ¬i)` be lower @@ -675,10 +667,8 @@ the empirical means as estimator satisfies `𝔼[τ_δ] ≤ c log (1 / δ)` for every `c > (inf_{v ∈ C} D(μ, v, ¬i))⁻¹`. -/ theorem eventually_expectedStoppingTime_cTrackAndStop_le (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hw_mem : ∀ μ', w μ' ∈ simplex α) {C : Set (α → ℝ)} (hC_conv : Convex ℝ C) (hC_compact : IsCompact C) (hw_tendsto : Tendsto w (𝓝 μ) (𝓝ˢ C)) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) @@ -731,7 +721,7 @@ theorem eventually_expectedStoppingTime_cTrackAndStop_le (hT : ∀ a c, ¬ T a = (K - 1) * (1 + √(n : ℝ))} have hE_sum : ∑' T, P (E T)ᶜ ≠ ∞ := by refine ne_top_of_le_ne_top (CTracking.tsum_measure_exists_ge_empMean_notMem_Ioo_ne_top hw0 hw1 - hseq hν_above hν_below hμ (fun a ↦ hlW.2.2.2 a) (fun a ↦ huW.2.2.2 a) hlμ hμu + hseq hν hμ (fun a ↦ hlW.2.2.2 a) (fun a ↦ huW.2.2.2 a) hlμ hμu tendsto_sqrt_roundsAfter_div_log) (tsum_le_tsum fun T ↦ measure_mono_ae ?_) filter_upwards [CTracking.abs_pullCount_sub_sum_le_mul_one_add_sqrt hw0 hw1 hseq] @@ -785,7 +775,7 @@ theorem eventually_expectedStoppingTime_cTrackAndStop_le (hT : ∀ a c, ¬ T a = /-- **Sample complexity of Track-and-Stop with C-tracking at the characteristic time** [DK19, Theorem 7], the upper bound `𝔼[τ_δ] ≤ c log (1 / δ)` with `c > T*(μ)`, even when the optimal allocations are not unique. Let the rewards of each arm `a` of the model `μ` be dominated -above and below by the member of mean `μ a` of a nondegenerate exponential family `(ρ a, T a)`, +on `Set.univ` by the member of mean `μ a` of a nondegenerate exponential family `(ρ a, T a)`, let `i` be the single correct answer of `μ`, let `(μ', w') ↦ D(μ', w', ¬i)` be continuous at every point `(μ, v)` with `v` in the simplex, on the allocations of the simplex, let the targets `w` be allocations, and optimal allocations `w(μ') ∈ w*(μ', ¬i)` near `μ`, and let the @@ -796,10 +786,8 @@ recommendation be `i` near `μ`. Then for thresholds `β δ n h ≤ log (r n / `w` to be continuous at `μ`. -/ theorem eventually_expectedStoppingTime_cTrackAndStop_le_of_charTime_lt (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hcorrect : task.correct μ = {i}) (hw_mem : ∀ μ', w μ' ∈ simplex α) (hw_opt : ∀ᶠ μ' in 𝓝 μ, w μ' ∈ task.optAlloc μ' i) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) (h_cont : ∀ v ∈ simplex α, ContinuousWithinAt @@ -821,7 +809,7 @@ theorem eventually_expectedStoppingTime_cTrackAndStop_le_of_charTime_lt have hw_tendsto : Tendsto w (𝓝 μ) (𝓝ˢ (task.optAlloc μ i)) := fun t ht ↦ by rw [Filter.mem_map] filter_upwards [h_uhc t ht, hw_opt] with μ' h1 h2 using subset_of_mem_nhdsSet h1 h2 - exact task.eventually_expectedStoppingTime_cTrackAndStop_le hT hμ hν_above hν_below hw_mem + exact task.eventually_expectedStoppingTime_cTrackAndStop_le hT hμ hν hw_mem (task.convex_optAlloc μ i) (task.isCompact_optAlloc h_usc) hw_tendsto hrec_eq (fun v hv ↦ (h_cont v (task.mem_optAlloc_iff.1 hv).1).lowerSemicontinuousWithinAt) hc' hr hβ @@ -853,10 +841,8 @@ Track-and-Stop with C-tracking and the thresholds `K log (2 n (n + 1)) + x_δ` s `limsup_{δ → 0} 𝔼[τ_δ] / log (1 / δ) ≤ T*(μ)`. -/ theorem eventually_expectedStoppingTime_cTrackAndStop_unionBoundThreshold_le (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hcorrect : task.correct μ = {i}) (hw_mem : ∀ μ', w μ' ∈ simplex α) (hw_opt : ∀ᶠ μ' in 𝓝 μ, w μ' ∈ task.optAlloc μ' i) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) (h_cont : ∀ v ∈ simplex α, ContinuousWithinAt @@ -869,7 +855,7 @@ theorem eventually_expectedStoppingTime_cTrackAndStop_unionBoundThreshold_le -- At the confidence level `δ ^ (1 / s)`, the thresholds are at most `log (r n / δ)` with -- `r n = (2 n (n + 1)) ^ K`. exact task.eventually_expectedStoppingTime_cTrackAndStop_le_of_charTime_lt (hw := hw) - (hrec := hrec) (hstop := fun δ' ↦ hstop (δ' ^ s⁻¹)) hT hμ hν_above hν_below hcorrect hw_mem + (hrec := hrec) (hstop := fun δ' ↦ hstop (δ' ^ s⁻¹)) hT hμ hν hcorrect hw_mem hw_opt hrec_eq h_cont hc' (isBigO_two_mul_mul_add_one_pow _) ((eventually_unionBoundThreshold_rpow_inv_le _ hs).mono fun _ h n hn _ ↦ h n hn) @@ -879,10 +865,8 @@ with `T*(μ) < ∞` that satisfies the assumptions of `IdentTask.eventually_expectedStoppingTime_cTrackAndStop_unionBoundThreshold_le`. -/ theorem stopsAS_cTrackAndStop_unionBoundThreshold (hT : ∀ a c, ¬ T a =ᵐ[ρ a] fun _ ↦ c) (hμ : ∀ a, μ a ∈ (ρ a).expFamilyMeans (T a)) - (hν_above : ∀ a, MGFDominatedAbove id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) - (hν_below : ∀ a, MGFDominatedBelow id (task.ν μ a) (T a) - ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a)))) + (hν : ∀ a, MGFDominatedOn id (task.ν μ a) (T a) + ((ρ a).expFamily (T a) ((ρ a).natParam (T a) (μ a))) Set.univ) (hcorrect : task.correct μ = {i}) (hw_mem : ∀ μ', w μ' ∈ simplex α) (hw_opt : ∀ᶠ μ' in 𝓝 μ, w μ' ∈ task.optAlloc μ' i) (hrec_eq : ∀ᶠ μ' in 𝓝 μ, rec μ' = i) (h_cont : ∀ v ∈ simplex α, ContinuousWithinAt @@ -895,7 +879,7 @@ theorem stopsAS_cTrackAndStop_unionBoundThreshold rw [ENNReal.coe_toNNReal h_charTime] exact ENNReal.lt_add_right h_charTime one_ne_zero have h := eventually_expectedStoppingTime_cTrackAndStop_unionBoundThreshold_le (hw := hw) - (hrec := hrec) (hstop := hstop) hT hμ hν_above hν_below hcorrect hw_mem hw_opt hrec_eq h_cont hc + (hrec := hrec) (hstop := hstop) hT hμ hν hcorrect hw_mem hw_opt hrec_eq h_cont hc simp only [cTrackAndStop_def] at h ⊢ exact stopsAS_glrt_unionBoundThreshold (h.mono fun _ hδ' ↦ ne_top_of_le_ne_top (ENNReal.mul_ne_top ENNReal.coe_ne_top ENNReal.ofReal_ne_top) hδ').frequently hδ hδ1 diff --git a/LMLExplore/Probability/Distributions/ExponentialFamily/Chernoff.lean b/LMLExplore/Probability/Distributions/ExponentialFamily/Chernoff.lean index 86338706..57f020c2 100644 --- a/LMLExplore/Probability/Distributions/ExponentialFamily/Chernoff.lean +++ b/LMLExplore/Probability/Distributions/ExponentialFamily/Chernoff.lean @@ -13,16 +13,18 @@ public import LMLExplore.Probability.Moments.MGF.Dominated Let `ρ` be a measure on a measurable space `𝓧` and `T : 𝓧 → ℝ` a statistic, with log-partition function `ψ = cgf T ρ`, and let `ρ_η(μ)` be the member of mean `μ` of their exponential family. A -real random variable `X` is dominated above by `ρ_η(μ)` if `E[exp (t X)] ≤ E_{ρ_η(μ)}[exp (t T)]` -for every `t ≥ 0` (`LMLExplore.MGFDominatedAbove X P T ρ_η(μ)`), and dominated below if the same -holds for every `t ≤ 0`. +real random variable `X` is dominated by `ρ_η(μ)` on `Set.Ici 0` if +`E[exp (t X)] ≤ E_{ρ_η(μ)}[exp (t T)]` for every `t ≥ 0` +(`LMLExplore.MGFDominatedOn X P T ρ_η(μ) (Set.Ici 0)`), and on `Set.Iic 0` if the same holds for +every `t ≤ 0`. -For independent random variables `X i`, `i ∈ s`, dominated above by `ρ_η(μ)` and a mean `x ≥ μ` of +For independent random variables `X i`, `i ∈ s`, dominated by `ρ_η(μ)` on `Set.Ici 0` and a mean +`x ≥ μ` of the family, the probability that the empirical mean of the `X i` is at least `x` decays exponentially in the number `#s` of variables, at the rate given by the Kullback–Leibler divergence `d(x, μ) = KL(ρ_η(x), ρ_η(μ))`: `P(#s * x ≤ ∑ i ∈ s, X i) ≤ exp (-(#s * d(x, μ)))`, and -symmetrically for the lower tail of variables dominated below. The statistics `T (Y i)` of -independent observations `Y i` with law `ρ_η(μ)` are dominated above and below, which gives these +symmetrically for the lower tail of variables dominated on `Set.Iic 0`. The statistics `T (Y i)` of +independent observations `Y i` with law `ρ_η(μ)` are dominated on every set, which gives these bounds for the sums `∑ i ∈ s, T (Y i)`; for a natural exponential family on `ℝ` (`T = id`), these are bounds on the sums `∑ i ∈ s, Y i` themselves. @@ -43,11 +45,11 @@ with values in `[0, 1]` are dominated by Bernoulli laws, which gives the bounds ## Main statements * `ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_exp_expFamilyDiv`: the upper tail - `P(#s * x ≤ ∑ i ∈ s, X i) ≤ exp (-(#s * d(x, μ)))` for variables dominated above by the member - of mean `μ` and means `μ ≤ x` of the family. + `P(#s * x ≤ ∑ i ∈ s, X i) ≤ exp (-(#s * d(x, μ)))` for variables dominated by the member of + mean `μ` on `Set.Ici 0` and means `μ ≤ x` of the family. * `ProbabilityTheory.iIndepFun.measureReal_sum_le_le_exp_expFamilyDiv`: the lower tail - `P(∑ i ∈ s, X i ≤ #s * x) ≤ exp (-(#s * d(x, μ)))` for variables dominated below by the member - of mean `μ` and means `x ≤ μ` of the family. + `P(∑ i ∈ s, X i ≤ #s * x) ≤ exp (-(#s * d(x, μ)))` for variables dominated by the member of + mean `μ` on `Set.Iic 0` and means `x ≤ μ` of the family. * `ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_exp_expFamilyDiv_of_hasLaw`, `ProbabilityTheory.iIndepFun.measureReal_sum_le_le_exp_expFamilyDiv_of_hasLaw`: the same bounds for the statistics `T (Y i)` of independent observations `Y i` with law the member of mean `μ`. @@ -104,28 +106,28 @@ private lemma integrable_and_exp_mul_mgf_pow_natParam_le (hμ : μ ∈ ρ.expFam ring_nf /-- **Cramér–Chernoff bound under domination by an exponential family, upper tail.** For -independent random variables `X i`, `i ∈ s`, dominated above by the member `ρ_η(μ)` of mean `μ` -of the exponential family of `ρ` and `T`, and a mean `x ≥ μ` of the family, +independent random variables `X i`, `i ∈ s`, dominated on `Set.Ici 0` by the member `ρ_η(μ)` of +mean `μ` of the exponential family of `ρ` and `T`, and a mean `x ≥ μ` of the family, `P(#s * x ≤ ∑ i ∈ s, X i) ≤ exp (-(#s * d(x, μ)))`, where `d(x, μ) = KL(ρ_η(x), ρ_η(μ))`. -/ theorem iIndepFun.measureReal_sum_ge_le_exp_expFamilyDiv (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedAbove (X i) P T (ρ.expFamily T (ρ.natParam T μ))) + (hX : ∀ i ∈ s, MGFDominatedOn (X i) P T (ρ.expFamily T (ρ.natParam T μ)) (Set.Ici 0)) (hμ : μ ∈ ρ.expFamilyMeans T) (hx : x ∈ ρ.expFamilyMeans T) (hμx : μ ≤ x) : P.real {ω | #s * x ≤ ∑ i ∈ s, X i ω} ≤ exp (-(#s * ρ.expFamilyDiv T x μ)) := by obtain ⟨h_int, h_le⟩ := integrable_and_exp_mul_mgf_pow_natParam_le hμ hx #s - exact (h_indep.measureReal_sum_ge_le_exp_mul_mgf_pow hX _ - (sub_nonneg.2 (Measure.monotoneOn_natParam hμ hx hμx)) h_int).trans h_le + have ht := sub_nonneg.2 (Measure.monotoneOn_natParam hμ hx hμx) + exact (h_indep.measureReal_sum_ge_le_exp_mul_mgf_pow hX _ ht ht h_int).trans h_le /-- **Cramér–Chernoff bound under domination by an exponential family, lower tail.** For -independent random variables `X i`, `i ∈ s`, dominated below by the member `ρ_η(μ)` of mean `μ` -of the exponential family of `ρ` and `T`, and a mean `x ≤ μ` of the family, +independent random variables `X i`, `i ∈ s`, dominated on `Set.Iic 0` by the member `ρ_η(μ)` of +mean `μ` of the exponential family of `ρ` and `T`, and a mean `x ≤ μ` of the family, `P(∑ i ∈ s, X i ≤ #s * x) ≤ exp (-(#s * d(x, μ)))`, where `d(x, μ) = KL(ρ_η(x), ρ_η(μ))`. -/ theorem iIndepFun.measureReal_sum_le_le_exp_expFamilyDiv (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedBelow (X i) P T (ρ.expFamily T (ρ.natParam T μ))) + (hX : ∀ i ∈ s, MGFDominatedOn (X i) P T (ρ.expFamily T (ρ.natParam T μ)) (Set.Iic 0)) (hμ : μ ∈ ρ.expFamilyMeans T) (hx : x ∈ ρ.expFamilyMeans T) (hxμ : x ≤ μ) : P.real {ω | ∑ i ∈ s, X i ω ≤ #s * x} ≤ exp (-(#s * ρ.expFamilyDiv T x μ)) := by obtain ⟨h_int, h_le⟩ := integrable_and_exp_mul_mgf_pow_natParam_le hμ hx #s - exact (h_indep.measureReal_sum_le_le_exp_mul_mgf_pow hX _ - (sub_nonpos.2 (Measure.monotoneOn_natParam hx hμ hxμ)) h_int).trans h_le + have ht := sub_nonpos.2 (Measure.monotoneOn_natParam hx hμ hxμ) + exact (h_indep.measureReal_sum_le_le_exp_mul_mgf_pow hX _ ht ht h_int).trans h_le /-! ### Observations with law a member of the family -/ @@ -156,7 +158,7 @@ theorem iIndepFun.measureReal_sum_ge_le_exp_expFamilyDiv_of_hasLaw (h_indep : iI Finset.sum_coe_sort s fun i ↦ T (Y i ω) simpa only [card_univ, Fintype.card_coe, h_sum] using h_indep'.measureReal_sum_ge_le_exp_expFamilyDiv (s := univ) - (fun i _ ↦ (h_ident i).mgfDominatedAbove) hμ hx hμx + (fun i _ ↦ (h_ident i).mgfDominatedOn) hμ hx hμx /-- **Cramér–Chernoff bound for an exponential family, lower tail.** For independent random variables `Y i`, `i ∈ s`, with law the member `ρ_η(μ)` of mean `μ` of the exponential family of `ρ` @@ -172,6 +174,6 @@ theorem iIndepFun.measureReal_sum_le_le_exp_expFamilyDiv_of_hasLaw (h_indep : iI Finset.sum_coe_sort s fun i ↦ T (Y i ω) simpa only [card_univ, Fintype.card_coe, h_sum] using h_indep'.measureReal_sum_le_le_exp_expFamilyDiv (s := univ) - (fun i _ ↦ (h_ident i).mgfDominatedBelow) hμ hx hxμ + (fun i _ ↦ (h_ident i).mgfDominatedOn) hμ hx hxμ end ProbabilityTheory diff --git a/LMLExplore/Probability/Moments/KLChernoff.lean b/LMLExplore/Probability/Moments/KLChernoff.lean index af6ac069..aef6f2c5 100644 --- a/LMLExplore/Probability/Moments/KLChernoff.lean +++ b/LMLExplore/Probability/Moments/KLChernoff.lean @@ -23,11 +23,11 @@ their sum over a finite set `s` exceeds `#s * p`, for `p ∈ [m, 1]`, is at most `exp (-#s * d(p, m))`, where `d = klBerReal` is the binary relative entropy. Symmetrically, if the means are at least `m`, the probability that the sum is at most `#s * p`, for `p ∈ [0, m]`, is at most `exp (-#s * d(p, m))`. This is the Chernoff bound of the Bernoulli law, which dominates the -`[0, 1]`-valued case: by convexity of `exp`, `E[exp (t X)] ≤ 1 - m + m exp t` for `t ≥ 0`, so that -`X` is dominated above by `Ber((1 : ℝ), 0, m)` (`LMLExplore.MGFDominatedAbove`), and symmetrically -dominated below when its mean is at least `m`. The Bernoulli laws form an exponential family whose -divergence is `d`, and for `p, m ∈ (0, 1)` both bounds are the Cramér–Chernoff bounds under -domination by an exponential family +`[0, 1]`-valued case: by convexity of `exp`, `E[exp (t X)] ≤ 1 - m + m exp t` for `t ≥ 0`, so +that `X` is dominated by `Ber((1 : ℝ), 0, m)` on `Set.Ici 0` (`LMLExplore.MGFDominatedOn`), and +symmetrically on `Set.Iic 0` when its mean is at least `m`. The Bernoulli laws form an exponential +family whose divergence is `d`, and for `p, m ∈ (0, 1)` both bounds are the Cramér–Chernoff bounds +under domination by an exponential family (`ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_exp_expFamilyDiv`). At the boundary levels `p = 1` (upper tail) and `p = 0` (lower tail), the bounds `m ^ #s` and `(1 - m) ^ #s` follow from Markov's inequality, since the sum reaches `#s` (resp. `0`) only if every `X i` is `1` @@ -50,9 +50,10 @@ expected number of sample sizes `s` at which `s = 0`, `c ≤ μ̂_s` or `d(μ̂_ `t`, `mgf X μ t ≤ 1 - E[X] + E[X] exp t`. * `LMLExplore.mgf_le_one_sub_add_mul_exp`: for `X ∈ [0, 1]` a.s. with `E[X] ≤ m` and `t ≥ 0`, `mgf X μ t ≤ 1 - m + m exp t`. -* `LMLExplore.mgfDominatedAbove_bernoulliMeasure`, `LMLExplore.mgfDominatedBelow_bernoulliMeasure`: - a random variable with values in `[0, 1]` and mean at most (resp. at least) `q` is dominated - above (resp. below) by `Ber((1 : ℝ), 0, q)`. +* `LMLExplore.mgfDominatedOn_Ici_bernoulliMeasure`, + `LMLExplore.mgfDominatedOn_Iic_bernoulliMeasure`: a random variable with values in `[0, 1]` and + mean at most (resp. at least) `q` is dominated by `Ber((1 : ℝ), 0, q)` on `Set.Ici 0` (resp. + `Set.Iic 0`). * `LMLExplore.measureReal_sum_ge_le_exp_klBerReal`: the upper tail `P(#s * p ≤ ∑ i ∈ s, X i) ≤ exp (-(#s * d(p, m)))` for `0 < m ≤ p ≤ 1`. * `LMLExplore.measureReal_card_mul_add_le_sum_le`: Hoeffding's inequality @@ -121,21 +122,21 @@ theorem mgf_le_one_sub_add_mul_exp [IsProbabilityMeasure μ] {X : Ω → ℝ} (h have := mul_le_mul_of_nonneg_right hmean (sub_nonneg.2 (one_le_exp ht)) linarith [mgf_le_one_sub_integral_add_integral_mul_exp hXm hX t] -/-- A random variable with values in `[0, 1]` and mean at most `q` is dominated above by the -Bernoulli law of mean `q`: `mgf X μ t ≤ mgf id Ber((1 : ℝ), 0, q) t` for `t ≥ 0`. -/ -theorem mgfDominatedAbove_bernoulliMeasure [IsProbabilityMeasure μ] {X : Ω → ℝ} +/-- A random variable with values in `[0, 1]` and mean at most `q` is dominated by the Bernoulli +law of mean `q` on `Set.Ici 0`: `mgf X μ t ≤ mgf id Ber((1 : ℝ), 0, q) t` for `t ≥ 0`. -/ +theorem mgfDominatedOn_Ici_bernoulliMeasure [IsProbabilityMeasure μ] {X : Ω → ℝ} (hXm : AEMeasurable X μ) (hX : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) {q : I} (hmean : μ[X] ≤ (q : ℝ)) : - MGFDominatedAbove X μ id Ber((1 : ℝ), 0, q) where + MGFDominatedOn X μ id Ber((1 : ℝ), 0, q) (Set.Ici 0) where integrable_exp_mul _ _ _ := integrable_exp_mul_of_mem_Icc hXm hX mgf_le _ ht _ := by rw [TauCeti.Probability.mgf_id_bernoulliMeasure] exact mgf_le_one_sub_add_mul_exp hXm hX hmean ht -/-- A random variable with values in `[0, 1]` and mean at least `q` is dominated below by the -Bernoulli law of mean `q`: `mgf X μ t ≤ mgf id Ber((1 : ℝ), 0, q) t` for `t ≤ 0`. -/ -theorem mgfDominatedBelow_bernoulliMeasure [IsProbabilityMeasure μ] {X : Ω → ℝ} +/-- A random variable with values in `[0, 1]` and mean at least `q` is dominated by the Bernoulli +law of mean `q` on `Set.Iic 0`: `mgf X μ t ≤ mgf id Ber((1 : ℝ), 0, q) t` for `t ≤ 0`. -/ +theorem mgfDominatedOn_Iic_bernoulliMeasure [IsProbabilityMeasure μ] {X : Ω → ℝ} (hXm : AEMeasurable X μ) (hX : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) {q : I} (hmean : (q : ℝ) ≤ μ[X]) : - MGFDominatedBelow X μ id Ber((1 : ℝ), 0, q) where + MGFDominatedOn X μ id Ber((1 : ℝ), 0, q) (Set.Iic 0) where integrable_exp_mul _ _ _ := integrable_exp_mul_of_mem_Icc hXm hX mgf_le t ht _ := by rw [TauCeti.Probability.mgf_id_bernoulliMeasure] @@ -192,8 +193,8 @@ theorem measureReal_sum_ge_le_exp_klBerReal {X : ι → Ω → ℝ} (h_indep : i · -- `p = 1`: the sum reaches `#s` with probability at most `m ^ #s = exp (-(#s * d(1, m)))` rw [mul_one, klBerReal_one_left, mul_neg, neg_neg, exp_nat_mul, exp_log hm] exact measureReal_card_le_sum_le_pow h_indep hXm hX hmean - · -- `m < p < 1`: the `X i` are dominated above by `Ber(1, 0, m)`, the member of mean `m` of the - -- exponential family of `Ber(1, 0, 1/2)`, whose divergence is `d` + · -- `m < p < 1`: the `X i` are dominated on `Set.Ici 0` by `Ber(1, 0, m)`, the member of mean + -- `m` of the exponential family of `Ber(1, 0, 1/2)`, whose divergence is `d` have hm' : m ∈ Set.Ioo 0 1 := ⟨hm, hm1⟩ have hp' : p ∈ Set.Ioo 0 1 := ⟨hm.trans hmp, hp1⟩ rw [← expFamilyDiv_bernoulliMeasure_sigmoid 0 hp' hm'] @@ -201,7 +202,7 @@ theorem measureReal_sum_ge_le_exp_klBerReal {X : ι → Ω → ℝ} (h_indep : i (by rwa [expFamilyMeans_bernoulliMeasure_sigmoid]) (by rwa [expFamilyMeans_bernoulliMeasure_sigmoid]) hmp.le rw [expFamily_natParam_bernoulliMeasure_sigmoid 0 hm'] - exact mgfDominatedAbove_bernoulliMeasure (hXm i hi) (hX i hi) (hmean i hi) + exact mgfDominatedOn_Ici_bernoulliMeasure (hXm i hi) (hX i hi) (hmean i hi) /-- **Hoeffding's inequality** for independent random variables `X i ∈ [0, 1]` with means at most `m`: for `ε ≥ 0`, `P(#s * (m + ε) ≤ ∑ i ∈ s, X i) ≤ exp (-2 ε² #s)`. -/ @@ -261,8 +262,8 @@ theorem measureReal_sum_le_le_exp_klBerReal {X : ι → Ω → ℝ} (h_indep : i ext ω simp only [Set.mem_ofPred_eq, mul_zero, sum_sub_distrib, sum_const, nsmul_eq_mul, mul_one] constructor <;> intro h <;> linarith - · -- `0 < p < m`: the `X i` are dominated below by `Ber(1, 0, m)`, the member of mean `m` of the - -- exponential family of `Ber(1, 0, 1/2)`, whose divergence is `d` + · -- `0 < p < m`: the `X i` are dominated on `Set.Iic 0` by `Ber(1, 0, m)`, the member of mean + -- `m` of the exponential family of `Ber(1, 0, 1/2)`, whose divergence is `d` have hm' : m ∈ Set.Ioo 0 1 := ⟨hm0, hm⟩ have hp' : p ∈ Set.Ioo 0 1 := ⟨hp0, hpm.trans hm⟩ rw [← expFamilyDiv_bernoulliMeasure_sigmoid 0 hp' hm'] @@ -270,7 +271,7 @@ theorem measureReal_sum_le_le_exp_klBerReal {X : ι → Ω → ℝ} (h_indep : i (by rwa [expFamilyMeans_bernoulliMeasure_sigmoid]) (by rwa [expFamilyMeans_bernoulliMeasure_sigmoid]) hpm.le rw [expFamily_natParam_bernoulliMeasure_sigmoid 0 hm'] - exact mgfDominatedBelow_bernoulliMeasure (hXm i hi) (hX i hi) (hmean i hi) + exact mgfDominatedOn_Iic_bernoulliMeasure (hXm i hi) (hX i hi) (hmean i hi) /-- **Chernoff bound in relative-entropy form, lower tail, for a set of levels** ([LS, (10.3) of Corollary 10.4]): for independent random variables `X i ∈ [0, 1]` with means at diff --git a/LMLExplore/Probability/Moments/MGF/Bound.lean b/LMLExplore/Probability/Moments/MGF/Bound.lean index 79341367..77c98664 100644 --- a/LMLExplore/Probability/Moments/MGF/Bound.lean +++ b/LMLExplore/Probability/Moments/MGF/Bound.lean @@ -16,9 +16,9 @@ public import Mathlib.Probability.Distributions.Gaussian.Real For a real random variable `X`, a function `ψ : ℝ → ℝ` and a set `Λ ⊆ ℝ` of parameters, `X` has its moment generating function bounded by `exp ψ` on `Λ` if `E[exp (t X)] ≤ exp (ψ t)` for every `t ∈ Λ`. Sub-Gaussian variables are the case `ψ t = c t ^ 2 / 2` on `ℝ`, sub-exponential variables -the case `ψ t = V t ^ 2 / 2` on `{t | b |t| ≤ 1}`, and a variable dominated above by a variable `Y` -in the sense of `LMLExplore.MGFDominatedAbove` is the case of the cumulant generating function of -`Y` on the nonnegative parameters where it is finite. One definition with a free `ψ` lets the +the case `ψ t = V t ^ 2 / 2` on `{t | b |t| ≤ 1}`, and a variable dominated by a variable `Y` on a +set `Λ` in the sense of `LMLExplore.MGFDominatedOn` is the case of the cumulant generating function +of `Y` on the parameters of `Λ` where it is finite. One definition with a free `ψ` lets the exponential supermartingales, and the time-uniform deviation bounds built from them, be proved once for all these classes (see `LMLExplore.Probability.Martingale.MGFBound`). @@ -63,8 +63,8 @@ weights of an exponential supermartingale. versions (`ProbabilityTheory.Kernel.hasMGFBound_iff_hasSubgaussianMGF`, …) and the unconditional ones (`LMLExplore.hasMGFBound_iff_hasSubgaussianMGF`, `LMLExplore.hasMGFBound_iff_hasSubexponentialMGF`). -* `LMLExplore.mgfDominatedAbove_iff_hasMGFBound`, `LMLExplore.mgfDominatedBelow_iff_hasMGFBound`: - domination by `Y` is the bound by the cumulant generating function of `Y`. +* `LMLExplore.mgfDominatedOn_iff_hasMGFBound`: domination by `Y` on `Λ` is the bound by the + cumulant generating function of `Y` on `Λ`. * `ProbabilityTheory.HasCondSubgaussianMGF.hasCondMGFBound_cgf_gaussianReal`: if `X - a` is conditionally `c`-sub-Gaussian, the moment generating function of `X` is conditionally bounded by that of the Gaussian law of mean `a` and variance `c`. @@ -392,21 +392,10 @@ end SubgaussianSubexponential variable {P : Measure Ω} {Q : Measure Ω'} [NeZero Q] {Y : Ω' → ℝ} -/-- `X` under `P` is dominated above by `Y` under `Q` iff its moment generating function is -bounded by `exp (cgf Y Q)` on the nonnegative parameters at which `exp (t * Y)` is -`Q`-integrable. -/ -lemma mgfDominatedAbove_iff_hasMGFBound : - MGFDominatedAbove X P Y Q ↔ HasMGFBound X (cgf Y Q) (Set.Ici 0 ∩ integrableExpSet Y Q) P := - ⟨fun h ↦ ⟨fun _ ht ↦ h.integrable_exp_mul ht.1 ht.2, - fun _ ht ↦ (exp_cgf ht.2).symm ▸ h.mgf_le ht.1 ht.2⟩, - fun h ↦ ⟨fun _ ht hY ↦ h.integrable_exp_mul ⟨ht, hY⟩, - fun _ ht hY ↦ exp_cgf hY ▸ h.mgf_le ⟨ht, hY⟩⟩⟩ - -/-- `X` under `P` is dominated below by `Y` under `Q` iff its moment generating function is -bounded by `exp (cgf Y Q)` on the nonpositive parameters at which `exp (t * Y)` is -`Q`-integrable. -/ -lemma mgfDominatedBelow_iff_hasMGFBound : - MGFDominatedBelow X P Y Q ↔ HasMGFBound X (cgf Y Q) (Set.Iic 0 ∩ integrableExpSet Y Q) P := +/-- `X` under `P` is dominated by `Y` under `Q` on `Λ` iff its moment generating function is +bounded by `exp (cgf Y Q)` on the parameters of `Λ` at which `exp (t * Y)` is `Q`-integrable. -/ +lemma mgfDominatedOn_iff_hasMGFBound : + MGFDominatedOn X P Y Q Λ ↔ HasMGFBound X (cgf Y Q) (Λ ∩ integrableExpSet Y Q) P := ⟨fun h ↦ ⟨fun _ ht ↦ h.integrable_exp_mul ht.1 ht.2, fun _ ht ↦ (exp_cgf ht.2).symm ▸ h.mgf_le ht.1 ht.2⟩, fun h ↦ ⟨fun _ ht hY ↦ h.integrable_exp_mul ⟨ht, hY⟩, diff --git a/LMLExplore/Probability/Moments/MGF/Dominated.lean b/LMLExplore/Probability/Moments/MGF/Dominated.lean index 11772f30..a3b4797d 100644 --- a/LMLExplore/Probability/Moments/MGF/Dominated.lean +++ b/LMLExplore/Probability/Moments/MGF/Dominated.lean @@ -11,43 +11,41 @@ public import Mathlib.Probability.Moments.Basic /-! # Domination of moment generating functions and Chernoff bounds -A real random variable `X` under a measure `P` is *dominated above* by a real random variable `Y` -under a measure `Q` if `E_P[exp (t X)] ≤ E_Q[exp (t Y)]` for every `t ≥ 0`, as an inequality in -`[0, ∞]`: at each `t ≥ 0` where `exp (t Y)` is `Q`-integrable, `exp (t X)` is `P`-integrable and -`mgf X P t ≤ mgf Y Q t`. It is *dominated below* if the same holds for every `t ≤ 0`. For example, -a random variable with values in `[0, 1]` and mean at most `m` is dominated above by the Bernoulli -law of mean `m`, and identically distributed random variables dominate each other. +A real random variable `X` under a measure `P` is *dominated* by a real random variable `Y` under +a measure `Q` on a set `Λ` of parameters if `E_P[exp (t X)] ≤ E_Q[exp (t Y)]` for every `t ∈ Λ`, +as an inequality in `[0, ∞]`: at each `t ∈ Λ` where `exp (t Y)` is `Q`-integrable, `exp (t X)` is +`P`-integrable and `mgf X P t ≤ mgf Y Q t`. Domination on `Set.Ici 0` gives the Chernoff bounds of +the upper tail, domination on `Set.Iic 0` those of the lower tail, and domination on `Set.univ` +both. For example, a random variable with values in `[0, 1]` and mean at most `m` is dominated by +the Bernoulli law of mean `m` on `Set.Ici 0`, and identically distributed random variables dominate +each other on every set. The Chernoff bound transfers through the domination: the sum `∑ i ∈ s, X i` of independent random -variables dominated above by `Y` satisfies, for `t ≥ 0`, +variables dominated by `Y` on `Λ` satisfies, for `t ∈ Λ` with `t ≥ 0`, `P(a ≤ ∑ i ∈ s, X i) ≤ exp (-t a) (mgf Y Q t) ^ #s`, the Chernoff bound of a sum of `#s` -independent copies of `Y`; symmetrically for the lower tail. With `Y` the statistic of an -exponential family, this gives Cramér–Chernoff bounds for random variables that are dominated by a -member of the family without following its law. +independent copies of `Y`; symmetrically for the lower tail and `t ≤ 0`. With `Y` the statistic of +an exponential family, this gives Cramér–Chernoff bounds for random variables that are dominated +by a member of the family without following its law. ## Main definitions -* `LMLExplore.MGFDominatedAbove X P Y Q`: `E_P[exp (t X)] ≤ E_Q[exp (t Y)]` for every `t ≥ 0`. -* `LMLExplore.MGFDominatedBelow X P Y Q`: `E_P[exp (t X)] ≤ E_Q[exp (t Y)]` for every `t ≤ 0`. +* `LMLExplore.MGFDominatedOn X P Y Q Λ`: `E_P[exp (t X)] ≤ E_Q[exp (t Y)]` for every `t ∈ Λ`. ## Main statements -* `ProbabilityTheory.IdentDistrib.mgfDominatedAbove`, - `ProbabilityTheory.IdentDistrib.mgfDominatedBelow`: identically distributed random variables - dominate each other. -* `LMLExplore.MGFDominatedAbove.neg`, `LMLExplore.MGFDominatedBelow.neg`: `X` is dominated above - by `Y` iff `-X` is dominated below by `-Y`. -* `LMLExplore.MGFDominatedAbove.trans`, `LMLExplore.MGFDominatedBelow.trans`: domination is +* `ProbabilityTheory.IdentDistrib.mgfDominatedOn`: identically distributed random variables + dominate each other on every set. +* `LMLExplore.MGFDominatedOn.mono`, `LMLExplore.MGFDominatedOn.neg`, + `LMLExplore.MGFDominatedOn.trans`: domination on `Λ` implies domination on every subset of `Λ`; + if `X` is dominated by `Y` on `Λ`, then `-X` is dominated by `-Y` on `-Λ`; domination on `Λ` is transitive. -* `ProbabilityTheory.iIndepFun.mgf_sum_le_pow_of_mgfDominatedAbove`, - `ProbabilityTheory.iIndepFun.mgf_sum_le_pow_of_mgfDominatedBelow`: for independent `X i` - dominated above (resp. below) by `Y` and `t ≥ 0` (resp. `t ≤ 0`) with `exp (t Y)` integrable, +* `ProbabilityTheory.iIndepFun.mgf_sum_le_pow_of_mgfDominatedOn`: for independent `X i` dominated + by `Y` on `Λ` and `t ∈ Λ` with `exp (t Y)` integrable, `mgf (∑ i ∈ s, X i) P t ≤ (mgf Y Q t) ^ #s`. * `ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_exp_mul_mgf_pow`, `ProbabilityTheory.iIndepFun.measureReal_sum_le_le_exp_mul_mgf_pow`: the Chernoff bounds - `P(a ≤ ∑ i ∈ s, X i) ≤ exp (-t a) (mgf Y Q t) ^ #s` for `t ≥ 0` and variables dominated above, - and `P(∑ i ∈ s, X i ≤ a) ≤ exp (-t a) (mgf Y Q t) ^ #s` for `t ≤ 0` and variables dominated - below. + `P(a ≤ ∑ i ∈ s, X i) ≤ exp (-t a) (mgf Y Q t) ^ #s` for `t ∈ Λ` with `t ≥ 0`, and + `P(∑ i ∈ s, X i ≤ a) ≤ exp (-t a) (mgf Y Q t) ^ #s` for `t ∈ Λ` with `t ≤ 0`. ## References @@ -62,61 +60,41 @@ open MeasureTheory ProbabilityTheory Real Finset namespace LMLExplore variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : Measure Ω} - {Q : Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ} + {Q : Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ} {Λ Λ' : Set ℝ} -/-- A real random variable `X` under `P` is *dominated above* by `Y` under `Q` if -`E_P[exp (t X)] ≤ E_Q[exp (t Y)]` in `[0, ∞]` for every `t ≥ 0`: wherever `exp (t Y)` is +/-- A real random variable `X` under `P` is *dominated* by `Y` under `Q` on the set of parameters +`Λ` if `E_P[exp (t X)] ≤ E_Q[exp (t Y)]` in `[0, ∞]` for every `t ∈ Λ`: wherever `exp (t Y)` is `Q`-integrable, `exp (t X)` is `P`-integrable and `mgf X P t ≤ mgf Y Q t`. -/ -structure MGFDominatedAbove (X : Ω → ℝ) (P : Measure Ω) (Y : Ω' → ℝ) (Q : Measure Ω') : +structure MGFDominatedOn (X : Ω → ℝ) (P : Measure Ω) (Y : Ω' → ℝ) (Q : Measure Ω') (Λ : Set ℝ) : Prop where - integrable_exp_mul ⦃t : ℝ⦄ (ht : 0 ≤ t) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : + integrable_exp_mul ⦃t : ℝ⦄ (ht : t ∈ Λ) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : Integrable (fun ω ↦ exp (t * X ω)) P - mgf_le ⦃t : ℝ⦄ (ht : 0 ≤ t) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : + mgf_le ⦃t : ℝ⦄ (ht : t ∈ Λ) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : mgf X P t ≤ mgf Y Q t -/-- A real random variable `X` under `P` is *dominated below* by `Y` under `Q` if -`E_P[exp (t X)] ≤ E_Q[exp (t Y)]` in `[0, ∞]` for every `t ≤ 0`: wherever `exp (t Y)` is -`Q`-integrable, `exp (t X)` is `P`-integrable and `mgf X P t ≤ mgf Y Q t`. -/ -structure MGFDominatedBelow (X : Ω → ℝ) (P : Measure Ω) (Y : Ω' → ℝ) (Q : Measure Ω') : - Prop where - integrable_exp_mul ⦃t : ℝ⦄ (ht : t ≤ 0) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : - Integrable (fun ω ↦ exp (t * X ω)) P - mgf_le ⦃t : ℝ⦄ (ht : t ≤ 0) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : - mgf X P t ≤ mgf Y Q t +/-- Domination on `Λ` implies domination on every subset of `Λ`. -/ +lemma MGFDominatedOn.mono (h : MGFDominatedOn X P Y Q Λ) (hΛ : Λ' ⊆ Λ) : + MGFDominatedOn X P Y Q Λ' where + integrable_exp_mul _ ht hY := h.integrable_exp_mul (hΛ ht) hY + mgf_le _ ht hY := h.mgf_le (hΛ ht) hY -/-- If `X` is dominated above by `Y`, then `-X` is dominated below by `-Y`. -/ -lemma MGFDominatedAbove.neg (h : MGFDominatedAbove X P Y Q) : - MGFDominatedBelow (fun ω ↦ -X ω) P (fun ω ↦ -Y ω) Q where +/-- If `X` is dominated by `Y` on `Λ`, then `-X` is dominated by `-Y` on `-Λ`. -/ +lemma MGFDominatedOn.neg (h : MGFDominatedOn X P Y Q Λ) : + MGFDominatedOn (fun ω ↦ -X ω) P (fun ω ↦ -Y ω) Q (-Λ) where integrable_exp_mul t ht hY := by simpa only [mul_neg, neg_mul] using - h.integrable_exp_mul (neg_nonneg.2 ht) (by simpa only [mul_neg, neg_mul] using hY) + h.integrable_exp_mul (Set.mem_neg.1 ht) (by simpa only [mul_neg, neg_mul] using hY) mgf_le t ht hY := by simpa only [mgf, mul_neg, neg_mul] using - h.mgf_le (neg_nonneg.2 ht) (by simpa only [mul_neg, neg_mul] using hY) - -/-- If `X` is dominated below by `Y`, then `-X` is dominated above by `-Y`. -/ -lemma MGFDominatedBelow.neg (h : MGFDominatedBelow X P Y Q) : - MGFDominatedAbove (fun ω ↦ -X ω) P (fun ω ↦ -Y ω) Q where - integrable_exp_mul t ht hY := by - simpa only [mul_neg, neg_mul] using - h.integrable_exp_mul (neg_nonpos.2 ht) (by simpa only [mul_neg, neg_mul] using hY) - mgf_le t ht hY := by - simpa only [mgf, mul_neg, neg_mul] using - h.mgf_le (neg_nonpos.2 ht) (by simpa only [mul_neg, neg_mul] using hY) + h.mgf_le (Set.mem_neg.1 ht) (by simpa only [mul_neg, neg_mul] using hY) section Trans variable {Ω'' : Type*} {mΩ'' : MeasurableSpace Ω''} {R : Measure Ω''} {Z : Ω'' → ℝ} -/-- Domination above is transitive. -/ -lemma MGFDominatedAbove.trans (hXY : MGFDominatedAbove X P Y Q) - (hYZ : MGFDominatedAbove Y Q Z R) : MGFDominatedAbove X P Z R where - integrable_exp_mul _ ht hZ := hXY.integrable_exp_mul ht (hYZ.integrable_exp_mul ht hZ) - mgf_le _ ht hZ := (hXY.mgf_le ht (hYZ.integrable_exp_mul ht hZ)).trans (hYZ.mgf_le ht hZ) - -/-- Domination below is transitive. -/ -lemma MGFDominatedBelow.trans (hXY : MGFDominatedBelow X P Y Q) - (hYZ : MGFDominatedBelow Y Q Z R) : MGFDominatedBelow X P Z R where +/-- Domination on `Λ` is transitive. -/ +lemma MGFDominatedOn.trans (hXY : MGFDominatedOn X P Y Q Λ) (hYZ : MGFDominatedOn Y Q Z R Λ) : + MGFDominatedOn X P Z R Λ where integrable_exp_mul _ ht hZ := hXY.integrable_exp_mul ht (hYZ.integrable_exp_mul ht hZ) mgf_le _ ht hZ := (hXY.mgf_le ht (hYZ.integrable_exp_mul ht hZ)).trans (hYZ.mgf_le ht hZ) @@ -129,49 +107,33 @@ namespace ProbabilityTheory open LMLExplore variable {Ω Ω' ι : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : Measure Ω} - {Q : Measure Ω'} {X : ι → Ω → ℝ} {Y : Ω' → ℝ} {s : Finset ι} {t : ℝ} - -/-- Moment generating functions of identically distributed random variables agree, and so do -their exponential moments. -/ -private lemma IdentDistrib.integrable_exp_mul_and_mgf_eq {X : Ω → ℝ} (h : IdentDistrib X Y P Q) - (t : ℝ) : - (Integrable (fun ω ↦ exp (t * Y ω)) Q → Integrable (fun ω ↦ exp (t * X ω)) P) ∧ - mgf X P t = mgf Y Q t := by - have h' := h.comp (u := fun x ↦ exp (t * x)) (by fun_prop) - exact ⟨h'.integrable_iff.2, mgf_congr_of_identDistrib X Y h t⟩ - -/-- A random variable is dominated above by every random variable with the same law. -/ -lemma IdentDistrib.mgfDominatedAbove {X : Ω → ℝ} (h : IdentDistrib X Y P Q) : - MGFDominatedAbove X P Y Q := - ⟨fun t _ ↦ (h.integrable_exp_mul_and_mgf_eq t).1, - fun t _ _ ↦ (h.integrable_exp_mul_and_mgf_eq t).2.le⟩ - -/-- A random variable is dominated below by every random variable with the same law. -/ -lemma IdentDistrib.mgfDominatedBelow {X : Ω → ℝ} (h : IdentDistrib X Y P Q) : - MGFDominatedBelow X P Y Q := - ⟨fun t _ ↦ (h.integrable_exp_mul_and_mgf_eq t).1, - fun t _ _ ↦ (h.integrable_exp_mul_and_mgf_eq t).2.le⟩ - -/-- For independent random variables `X i`, `i ∈ s`, dominated above by `Y` under `Q`, and -`t ≥ 0` with `exp (t Y)` integrable, the sum `∑ i ∈ s, X i` has an exponential moment of + {Q : Measure Ω'} {X : ι → Ω → ℝ} {Y : Ω' → ℝ} {s : Finset ι} {t : ℝ} {Λ : Set ℝ} + +/-- A random variable is dominated on every set by every random variable with the same law. -/ +lemma IdentDistrib.mgfDominatedOn {X : Ω → ℝ} (h : IdentDistrib X Y P Q) : + MGFDominatedOn X P Y Q Λ where + integrable_exp_mul t _ := (h.comp (u := fun x ↦ exp (t * x)) (by fun_prop)).integrable_iff.2 + mgf_le t _ _ := (mgf_congr_of_identDistrib X Y h t).le + +/-- For independent random variables `X i`, `i ∈ s`, dominated by `Y` under `Q` on `Λ`, and +`t ∈ Λ` with `exp (t Y)` integrable, the sum `∑ i ∈ s, X i` has an exponential moment of order `t` and `mgf (∑ i ∈ s, X i) P t ≤ (mgf Y Q t) ^ #s`. -/ -private lemma iIndepFun.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_above - (h_indep : iIndepFun X P) (hX : ∀ i ∈ s, MGFDominatedAbove (X i) P Y Q) (ht : 0 ≤ t) +private lemma iIndepFun.integrable_exp_mul_sum_and_mgf_sum_le_pow + (h_indep : iIndepFun X P) (hX : ∀ i ∈ s, MGFDominatedOn (X i) P Y Q Λ) (ht : t ∈ Λ) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : Integrable (fun ω ↦ exp (t * ∑ i ∈ s, X i ω)) P ∧ mgf (fun ω ↦ ∑ i ∈ s, X i ω) P t ≤ mgf Y Q t ^ #s := by have := h_indep.isProbabilityMeasure - rcases ht.eq_or_lt with rfl | ht + rcases eq_or_ne t 0 with rfl | ht0 · -- at `t = 0`, both sides are total masses refine ⟨by simp, ?_⟩ rw [mgf_zero] rcases s.eq_empty_or_nonempty with rfl | ⟨i, hi⟩ · simp - · exact one_le_pow₀ ((mgf_zero (X := X i) (μ := P)).symm.trans_le ((hX i hi).mgf_le le_rfl hY)) - -- for `t > 0`, the exponential moments make the `X i` almost everywhere measurable + · exact one_le_pow₀ ((mgf_zero (X := X i) (μ := P)).symm.trans_le ((hX i hi).mgf_le ht hY)) + -- for `t ≠ 0`, the exponential moments make the `X i` almost everywhere measurable have h_meas (i : s) : AEMeasurable (X i) P := - aemeasurable_of_aemeasurable_exp_mul ht.ne' - ((hX i i.2).integrable_exp_mul ht.le hY).aemeasurable + aemeasurable_of_aemeasurable_exp_mul ht0 ((hX i i.2).integrable_exp_mul ht hY).aemeasurable have h_indep' : iIndepFun (fun i : s ↦ X i) P := h_indep.precomp Subtype.val_injective have h_sum : mgf (fun ω ↦ ∑ i ∈ s, X i ω) P t = ∏ i : s, mgf (X i) P t := by rw [← h_indep'.mgf_sum₀ h_meas univ] @@ -179,85 +141,53 @@ private lemma iIndepFun.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_above rw [Finset.sum_apply, Finset.sum_coe_sort s fun i ↦ X i ω] refine ⟨mgf_pos_iff.1 ?_, ?_⟩ · rw [h_sum] - exact Finset.prod_pos fun i _ ↦ mgf_pos ((hX i i.2).integrable_exp_mul ht.le hY) + exact Finset.prod_pos fun i _ ↦ mgf_pos ((hX i i.2).integrable_exp_mul ht hY) · rw [h_sum] calc ∏ i : s, mgf (X i) P t ≤ ∏ _i : s, mgf Y Q t := - prod_le_prod₀ (fun _ _ ↦ mgf_nonneg) fun i _ ↦ (hX i i.2).mgf_le ht.le hY + prod_le_prod₀ (fun _ _ ↦ mgf_nonneg) fun i _ ↦ (hX i i.2).mgf_le ht hY _ = mgf Y Q t ^ #s := by simp -/-- For independent random variables `X i`, `i ∈ s`, dominated above by `Y` under `Q`, and -`t ≥ 0` with `exp (t Y)` integrable, the sum `∑ i ∈ s, X i` has an exponential moment of +/-- For independent random variables `X i`, `i ∈ s`, dominated by `Y` under `Q` on `Λ`, and +`t ∈ Λ` with `exp (t Y)` integrable, the sum `∑ i ∈ s, X i` has an exponential moment of order `t`. -/ -theorem iIndepFun.integrable_exp_mul_sum_of_mgfDominatedAbove (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedAbove (X i) P Y Q) (ht : 0 ≤ t) +theorem iIndepFun.integrable_exp_mul_sum_of_mgfDominatedOn (h_indep : iIndepFun X P) + (hX : ∀ i ∈ s, MGFDominatedOn (X i) P Y Q Λ) (ht : t ∈ Λ) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : Integrable (fun ω ↦ exp (t * ∑ i ∈ s, X i ω)) P := - (h_indep.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_above hX ht hY).1 + (h_indep.integrable_exp_mul_sum_and_mgf_sum_le_pow hX ht hY).1 -/-- For independent random variables `X i`, `i ∈ s`, dominated above by `Y` under `Q`, and -`t ≥ 0` with `exp (t Y)` integrable, `mgf (∑ i ∈ s, X i) P t ≤ (mgf Y Q t) ^ #s`. -/ -theorem iIndepFun.mgf_sum_le_pow_of_mgfDominatedAbove (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedAbove (X i) P Y Q) (ht : 0 ≤ t) +/-- For independent random variables `X i`, `i ∈ s`, dominated by `Y` under `Q` on `Λ`, and +`t ∈ Λ` with `exp (t Y)` integrable, `mgf (∑ i ∈ s, X i) P t ≤ (mgf Y Q t) ^ #s`. -/ +theorem iIndepFun.mgf_sum_le_pow_of_mgfDominatedOn (h_indep : iIndepFun X P) + (hX : ∀ i ∈ s, MGFDominatedOn (X i) P Y Q Λ) (ht : t ∈ Λ) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : mgf (fun ω ↦ ∑ i ∈ s, X i ω) P t ≤ mgf Y Q t ^ #s := - (h_indep.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_above hX ht hY).2 + (h_indep.integrable_exp_mul_sum_and_mgf_sum_le_pow hX ht hY).2 /-- **Chernoff bound under domination, upper tail.** For independent random variables `X i`, -`i ∈ s`, dominated above by `Y` under `Q`, every threshold `a` and every `t ≥ 0` with -`exp (t Y)` integrable, `P(a ≤ ∑ i ∈ s, X i) ≤ exp (-t a) (mgf Y Q t) ^ #s`. -/ +`i ∈ s`, dominated by `Y` under `Q` on `Λ`, every threshold `a` and every `t ∈ Λ` with `t ≥ 0` +and `exp (t Y)` integrable, `P(a ≤ ∑ i ∈ s, X i) ≤ exp (-t a) (mgf Y Q t) ^ #s`. -/ theorem iIndepFun.measureReal_sum_ge_le_exp_mul_mgf_pow (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedAbove (X i) P Y Q) (a : ℝ) (ht : 0 ≤ t) + (hX : ∀ i ∈ s, MGFDominatedOn (X i) P Y Q Λ) (a : ℝ) (htΛ : t ∈ Λ) (ht : 0 ≤ t) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : P.real {ω | a ≤ ∑ i ∈ s, X i ω} ≤ exp (-t * a) * mgf Y Q t ^ #s := by have := h_indep.isProbabilityMeasure exact (measure_ge_le_exp_mul_mgf a ht - (h_indep.integrable_exp_mul_sum_of_mgfDominatedAbove hX ht hY)).trans - (mul_le_mul_of_nonneg_left (h_indep.mgf_sum_le_pow_of_mgfDominatedAbove hX ht hY) + (h_indep.integrable_exp_mul_sum_of_mgfDominatedOn hX htΛ hY)).trans + (mul_le_mul_of_nonneg_left (h_indep.mgf_sum_le_pow_of_mgfDominatedOn hX htΛ hY) (exp_pos _).le) -/-- For independent random variables `X i`, `i ∈ s`, dominated below by `Y` under `Q`, and -`t ≤ 0` with `exp (t Y)` integrable, the sum `∑ i ∈ s, X i` has an exponential moment of -order `t` and `mgf (∑ i ∈ s, X i) P t ≤ (mgf Y Q t) ^ #s`. -/ -private lemma iIndepFun.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_below - (h_indep : iIndepFun X P) (hX : ∀ i ∈ s, MGFDominatedBelow (X i) P Y Q) (ht : t ≤ 0) - (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : - Integrable (fun ω ↦ exp (t * ∑ i ∈ s, X i ω)) P ∧ - mgf (fun ω ↦ ∑ i ∈ s, X i ω) P t ≤ mgf Y Q t ^ #s := by - -- apply the upper-side statement to `-X i`, dominated above by `-Y`, at `-t ≥ 0` - have h_indep' : iIndepFun (fun i ω ↦ -X i ω) P := - h_indep.comp (fun _ x ↦ -x) fun _ ↦ measurable_neg - have h := h_indep'.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_above (fun i hi ↦ (hX i hi).neg) - (neg_nonneg.2 ht) (Y := fun ω ↦ -Y ω) (by simpa only [neg_mul_neg] using hY) - simpa only [mgf, Finset.sum_neg_distrib, neg_mul_neg] using h - -/-- For independent random variables `X i`, `i ∈ s`, dominated below by `Y` under `Q`, and -`t ≤ 0` with `exp (t Y)` integrable, the sum `∑ i ∈ s, X i` has an exponential moment of -order `t`. -/ -theorem iIndepFun.integrable_exp_mul_sum_of_mgfDominatedBelow (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedBelow (X i) P Y Q) (ht : t ≤ 0) - (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : - Integrable (fun ω ↦ exp (t * ∑ i ∈ s, X i ω)) P := - (h_indep.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_below hX ht hY).1 - -/-- For independent random variables `X i`, `i ∈ s`, dominated below by `Y` under `Q`, and -`t ≤ 0` with `exp (t Y)` integrable, `mgf (∑ i ∈ s, X i) P t ≤ (mgf Y Q t) ^ #s`. -/ -theorem iIndepFun.mgf_sum_le_pow_of_mgfDominatedBelow (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedBelow (X i) P Y Q) (ht : t ≤ 0) - (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : - mgf (fun ω ↦ ∑ i ∈ s, X i ω) P t ≤ mgf Y Q t ^ #s := - (h_indep.integrable_exp_mul_sum_and_mgf_sum_le_pow_of_below hX ht hY).2 - /-- **Chernoff bound under domination, lower tail.** For independent random variables `X i`, -`i ∈ s`, dominated below by `Y` under `Q`, every threshold `a` and every `t ≤ 0` with -`exp (t Y)` integrable, `P(∑ i ∈ s, X i ≤ a) ≤ exp (-t a) (mgf Y Q t) ^ #s`. -/ +`i ∈ s`, dominated by `Y` under `Q` on `Λ`, every threshold `a` and every `t ∈ Λ` with `t ≤ 0` +and `exp (t Y)` integrable, `P(∑ i ∈ s, X i ≤ a) ≤ exp (-t a) (mgf Y Q t) ^ #s`. -/ theorem iIndepFun.measureReal_sum_le_le_exp_mul_mgf_pow (h_indep : iIndepFun X P) - (hX : ∀ i ∈ s, MGFDominatedBelow (X i) P Y Q) (a : ℝ) (ht : t ≤ 0) + (hX : ∀ i ∈ s, MGFDominatedOn (X i) P Y Q Λ) (a : ℝ) (htΛ : t ∈ Λ) (ht : t ≤ 0) (hY : Integrable (fun ω ↦ exp (t * Y ω)) Q) : P.real {ω | ∑ i ∈ s, X i ω ≤ a} ≤ exp (-t * a) * mgf Y Q t ^ #s := by have := h_indep.isProbabilityMeasure exact (measure_le_le_exp_mul_mgf a ht - (h_indep.integrable_exp_mul_sum_of_mgfDominatedBelow hX ht hY)).trans - (mul_le_mul_of_nonneg_left (h_indep.mgf_sum_le_pow_of_mgfDominatedBelow hX ht hY) + (h_indep.integrable_exp_mul_sum_of_mgfDominatedOn hX htΛ hY)).trans + (mul_le_mul_of_nonneg_left (h_indep.mgf_sum_le_pow_of_mgfDominatedOn hX htΛ hY) (exp_pos _).le) end ProbabilityTheory diff --git a/LMLExplore/SequentialLearning/ExpFamilyDeviation.lean b/LMLExplore/SequentialLearning/ExpFamilyDeviation.lean index 90497e51..d6a26b73 100644 --- a/LMLExplore/SequentialLearning/ExpFamilyDeviation.lean +++ b/LMLExplore/SequentialLearning/ExpFamilyDeviation.lean @@ -12,8 +12,8 @@ public import LMLExplore.SequentialLearning.SumRewards /-! # Deviations of empirical means for rewards dominated by an exponential family -Let the rewards of arm `a` of a stochastic environment `Environment.bandit ν` be dominated above and -below by the member of mean `μ` of the exponential family of a measure `ρ` and a statistic `T`, +Let the rewards of arm `a` of a stochastic environment `Environment.bandit ν` be dominated on +`Set.univ` by the member of mean `μ` of the exponential family of a measure `ρ` and a statistic `T`, with divergence `d` in the mean parametrization. This file bounds the deviations of the empirical mean of `a`: first for the first `s` rewards in the reward stream model `streamMeasure ν`, by the Cramér–Chernoff bounds of `ExponentialFamily/Chernoff.lean`, then in a run of any algorithm, at all @@ -45,33 +45,33 @@ variable {α 𝓧 : Type*} [MeasurableSpace α] {m𝓧 : MeasurableSpace 𝓧} { [IsMarkovKernel ν] {ρ : Measure 𝓧} {T : 𝓧 → ℝ} {a : α} {μ x : ℝ} /-- **Cramér–Chernoff bound in the reward stream, upper tail.** If the rewards of arm `a` are -dominated above by the member of mean `μ` of the exponential family of `ρ` and `T`, then for a mean -`x ≥ μ` of the family, the sum of the first `s` rewards of `a` in the reward stream model is at -least `s x` with probability at most `exp (-(s d(x, μ)))`. -/ +dominated on `Set.Ici 0` by the member of mean `μ` of the exponential family of `ρ` and `T`, then +for a mean `x ≥ μ` of the family, the sum of the first `s` rewards of `a` in the reward stream +model is at least `s x` with probability at most `exp (-(s d(x, μ)))`. -/ theorem streamMeasure_sum_ge_le_exp_expFamilyDiv - (hν : MGFDominatedAbove id (ν a) T (ρ.expFamily T (ρ.natParam T μ))) + (hν : MGFDominatedOn id (ν a) T (ρ.expFamily T (ρ.natParam T μ)) (Set.Ici 0)) (hμ : μ ∈ ρ.expFamilyMeans T) (hx : x ∈ ρ.expFamilyMeans T) (hμx : μ ≤ x) (s : ℕ) : streamMeasure ν {ω | s * x ≤ ∑ i ∈ range s, ω i a} ≤ ENNReal.ofReal (exp (-(s * ρ.expFamilyDiv T x μ))) := by have h := (iIndepFun_eval_streamMeasure'' ν a).measureReal_sum_ge_le_exp_expFamilyDiv (s := range s) - (fun i _ ↦ (identDistrib_eval_eval_id_streamMeasure ν i a).mgfDominatedAbove.trans hν) hμ hx hμx + (fun i _ ↦ (identDistrib_eval_eval_id_streamMeasure ν i a).mgfDominatedOn.trans hν) hμ hx hμx rw [card_range] at h rw [← ofReal_measureReal] exact ENNReal.ofReal_le_ofReal h /-- **Cramér–Chernoff bound in the reward stream, lower tail.** If the rewards of arm `a` are -dominated below by the member of mean `μ` of the exponential family of `ρ` and `T`, then for a mean -`x ≤ μ` of the family, the sum of the first `s` rewards of `a` in the reward stream model is at -most `s x` with probability at most `exp (-(s d(x, μ)))`. -/ +dominated on `Set.Iic 0` by the member of mean `μ` of the exponential family of `ρ` and `T`, then +for a mean `x ≤ μ` of the family, the sum of the first `s` rewards of `a` in the reward stream +model is at most `s x` with probability at most `exp (-(s d(x, μ)))`. -/ theorem streamMeasure_sum_le_le_exp_expFamilyDiv - (hν : MGFDominatedBelow id (ν a) T (ρ.expFamily T (ρ.natParam T μ))) + (hν : MGFDominatedOn id (ν a) T (ρ.expFamily T (ρ.natParam T μ)) (Set.Iic 0)) (hμ : μ ∈ ρ.expFamilyMeans T) (hx : x ∈ ρ.expFamilyMeans T) (hxμ : x ≤ μ) (s : ℕ) : streamMeasure ν {ω | ∑ i ∈ range s, ω i a ≤ s * x} ≤ ENNReal.ofReal (exp (-(s * ρ.expFamilyDiv T x μ))) := by have h := (iIndepFun_eval_streamMeasure'' ν a).measureReal_sum_le_le_exp_expFamilyDiv (s := range s) - (fun i _ ↦ (identDistrib_eval_eval_id_streamMeasure ν i a).mgfDominatedBelow.trans hν) hμ hx hxμ + (fun i _ ↦ (identDistrib_eval_eval_id_streamMeasure ν i a).mgfDominatedOn.trans hν) hμ hx hxμ rw [card_range] at h rw [← ofReal_measureReal] exact ENNReal.ofReal_le_ofReal h @@ -87,14 +87,13 @@ variable {α 𝓧 : Type*} [DecidableEq α] [MeasurableSpace α] [Countable α] /-- **Deviations of the empirical mean of an arm with at least `m` pulls.** In a run of any algorithm against the stochastic bandit `Environment.bandit ν`, let the rewards of arm `a` be -dominated above and below by the member of mean `μ` of the exponential family of `ρ` and `T`, with +dominated on `Set.univ` by the member of mean `μ` of the exponential family of `ρ` and `T`, with divergence `d`, and let `l < μ < u` be means of the family. The probability that, at some round, `a` has at least `m` pulls and an empirical mean outside `(l, u)` is at most `exp (-m d(u, μ)) / (1 - exp (-d(u, μ))) + exp (-m d(l, μ)) / (1 - exp (-d(l, μ)))`. -/ theorem measure_exists_le_pullCount_and_empMean_notMem_Ioo_le (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) - (hν_above : MGFDominatedAbove id (ν a) T (ρ.expFamily T (ρ.natParam T μ))) - (hν_below : MGFDominatedBelow id (ν a) T (ρ.expFamily T (ρ.natParam T μ))) + (hν : MGFDominatedOn id (ν a) T (ρ.expFamily T (ρ.natParam T μ)) Set.univ) (hμ : μ ∈ ρ.expFamilyMeans T) (hl : l ∈ ρ.expFamilyMeans T) (hu : u ∈ ρ.expFamilyMeans T) (hlμ : l < μ) (hμu : μ < u) (m : ℕ) : P {ω | ∃ t, m ≤ pullCount A a t ω ∧ empMean A R a t ω ∉ Set.Ioo l u} ≤ @@ -120,8 +119,11 @@ theorem measure_exists_le_pullCount_and_empMean_notMem_Ioo_le _ ≤ ∑' k : ℕ, (ENNReal.ofReal (exp (-((k + m : ℕ) * ρ.expFamilyDiv T u μ))) + ENNReal.ofReal (exp (-((k + m : ℕ) * ρ.expFamilyDiv T l μ)))) := by refine tsum_le_tsum fun k ↦ (measure_union_le _ _).trans ?_ - exact (add_le_add (streamMeasure_sum_le_le_exp_expFamilyDiv hν_below hμ hl hlμ.le _) - (streamMeasure_sum_ge_le_exp_expFamilyDiv hν_above hμ hu hμu.le _)).trans_eq (add_comm _ _) + have h_lower := streamMeasure_sum_le_le_exp_expFamilyDiv (hν.mono (Set.subset_univ _)) hμ hl + hlμ.le (k + m) + have h_upper := streamMeasure_sum_ge_le_exp_expFamilyDiv (hν.mono (Set.subset_univ _)) hμ hu + hμu.le (k + m) + exact (add_le_add h_lower h_upper).trans_eq (add_comm _ _) _ = _ := by have h_tsum {d : ℝ} (hd : 0 < d) : ∑' k : ℕ, ENNReal.ofReal (exp (-((k + m : ℕ) * d))) = ENNReal.ofReal (exp (-(m * d)) / (1 - exp (-d))) := by From bc2420b9cf96fcc6f45eff530be76aac9abfe337 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 6 Nov 2026 08:04:11 +0100 Subject: [PATCH 2/2] feat: combine MGF domination on two sets of parameters Add mgfDominatedOn_union, MGFDominatedOn.union and MGFDominatedOn.univ_of_Iic_of_Ici, so that the one-sided producers on Set.Ici 0 and Set.Iic 0 reach the two-sided consumers on Set.univ. Co-Authored-By: Claude Code --- .../Probability/Moments/MGF/Dominated.lean | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/LMLExplore/Probability/Moments/MGF/Dominated.lean b/LMLExplore/Probability/Moments/MGF/Dominated.lean index a3b4797d..33ea76cc 100644 --- a/LMLExplore/Probability/Moments/MGF/Dominated.lean +++ b/LMLExplore/Probability/Moments/MGF/Dominated.lean @@ -39,6 +39,10 @@ by a member of the family without following its law. `LMLExplore.MGFDominatedOn.trans`: domination on `Λ` implies domination on every subset of `Λ`; if `X` is dominated by `Y` on `Λ`, then `-X` is dominated by `-Y` on `-Λ`; domination on `Λ` is transitive. +* `LMLExplore.mgfDominatedOn_union`, `LMLExplore.MGFDominatedOn.union`, + `LMLExplore.MGFDominatedOn.univ_of_Iic_of_Ici`: domination on `Λ ∪ Λ'` is domination on both + `Λ` and `Λ'`; in particular domination on `Set.Iic 0` and on `Set.Ici 0` gives domination on + `Set.univ`. * `ProbabilityTheory.iIndepFun.mgf_sum_le_pow_of_mgfDominatedOn`: for independent `X i` dominated by `Y` on `Λ` and `t ∈ Λ` with `exp (t Y)` integrable, `mgf (∑ i ∈ s, X i) P t ≤ (mgf Y Q t) ^ #s`. @@ -78,6 +82,25 @@ lemma MGFDominatedOn.mono (h : MGFDominatedOn X P Y Q Λ) (hΛ : Λ' ⊆ Λ) : integrable_exp_mul _ ht hY := h.integrable_exp_mul (hΛ ht) hY mgf_le _ ht hY := h.mgf_le (hΛ ht) hY +/-- Domination on `Λ ∪ Λ'` is domination on both `Λ` and `Λ'`. -/ +lemma mgfDominatedOn_union : + MGFDominatedOn X P Y Q (Λ ∪ Λ') ↔ MGFDominatedOn X P Y Q Λ ∧ MGFDominatedOn X P Y Q Λ' where + mp h := ⟨h.mono Set.subset_union_left, h.mono Set.subset_union_right⟩ + mpr h := + { integrable_exp_mul _ ht hY := + ht.elim (h.1.integrable_exp_mul · hY) (h.2.integrable_exp_mul · hY) + mgf_le _ ht hY := ht.elim (h.1.mgf_le · hY) (h.2.mgf_le · hY) } + +/-- Domination on `Λ` and on `Λ'` gives domination on `Λ ∪ Λ'`. -/ +lemma MGFDominatedOn.union (h : MGFDominatedOn X P Y Q Λ) (h' : MGFDominatedOn X P Y Q Λ') : + MGFDominatedOn X P Y Q (Λ ∪ Λ') := + mgfDominatedOn_union.2 ⟨h, h'⟩ + +/-- Domination on `Set.Iic 0` and on `Set.Ici 0` gives domination on `Set.univ`. -/ +lemma MGFDominatedOn.univ_of_Iic_of_Ici (h : MGFDominatedOn X P Y Q (Set.Iic 0)) + (h' : MGFDominatedOn X P Y Q (Set.Ici 0)) : MGFDominatedOn X P Y Q Set.univ := + (h.union h').mono Set.Iic_union_Ici.ge + /-- If `X` is dominated by `Y` on `Λ`, then `-X` is dominated by `-Y` on `-Λ`. -/ lemma MGFDominatedOn.neg (h : MGFDominatedOn X P Y Q Λ) : MGFDominatedOn (fun ω ↦ -X ω) P (fun ω ↦ -Y ω) Q (-Λ) where