diff --git a/LMLExplore/MeasureTheory/Function/ConditionalExpectation/Real.lean b/LMLExplore/MeasureTheory/Function/ConditionalExpectation/Real.lean new file mode 100644 index 00000000..27b490f6 --- /dev/null +++ b/LMLExplore/MeasureTheory/Function/ConditionalExpectation/Real.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic + +/-! +# Constant bounds on the conditional expectation of a bounded real function + +If an integrable real function `f` is at least `a` almost everywhere under a nonzero finite +measure `μ`, then its conditional expectation given a sub-σ-algebra `m` is at least `a` almost +everywhere, so an almost sure constant upper bound `μ[f | m] ≤ c` forces `a ≤ c`. Symmetrically, +if `f ≤ b` almost everywhere, an almost sure constant lower bound `c ≤ μ[f | m]` forces `c ≤ b`. +For instance, the conditional mean of a variable with values in `[0, 1]` cannot be bounded above +by a negative constant, nor below by a constant larger than `1`. + +## Main statements + +* `LMLExplore.le_of_ae_le_of_condExp_le`: if `a ≤ f` and `μ[f | m] ≤ c` almost everywhere, then + `a ≤ c`. +* `LMLExplore.le_of_le_condExp_of_ae_le`: if `c ≤ μ[f | m]` and `f ≤ b` almost everywhere, then + `c ≤ b`. +-/ + +public section + +open MeasureTheory + +namespace LMLExplore + +variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] [NeZero μ] + {f : Ω → ℝ} {a b c : ℝ} + +/-- If `a ≤ f` almost everywhere and the conditional expectation of `f` given a sub-σ-algebra `m` +is at most `c` almost everywhere, under a nonzero finite measure, then `a ≤ c`. -/ +lemma le_of_ae_le_of_condExp_le (hm : m ≤ mΩ) (hf : Integrable f μ) (ha : ∀ᵐ ω ∂μ, a ≤ f ω) + (hc : μ[f | m] ≤ᵐ[μ] fun _ ↦ c) : a ≤ c := by + have h := condExp_mono (m := m) (integrable_const a) hf ha + rw [condExp_const hm] at h + obtain ⟨_, h1, h2⟩ := (h.and hc).exists + exact h1.trans h2 + +/-- If the conditional expectation of `f` given a sub-σ-algebra `m` is at least `c` almost +everywhere and `f ≤ b` almost everywhere, under a nonzero finite measure, then `c ≤ b`. -/ +lemma le_of_le_condExp_of_ae_le (hm : m ≤ mΩ) (hf : Integrable f μ) + (hc : (fun _ ↦ c) ≤ᵐ[μ] μ[f | m]) (hb : ∀ᵐ ω ∂μ, f ω ≤ b) : c ≤ b := by + have h := condExp_mono (m := m) hf (integrable_const b) hb + rw [condExp_const hm] at h + obtain ⟨_, h1, h2⟩ := (hc.and h).exists + exact h1.trans h2 + +end LMLExplore diff --git a/LMLExplore/Probability/Kernel/Condexp.lean b/LMLExplore/Probability/Kernel/Condexp.lean index 3580775d..b2ba8e7b 100644 --- a/LMLExplore/Probability/Kernel/Condexp.lean +++ b/LMLExplore/Probability/Kernel/Condexp.lean @@ -9,7 +9,10 @@ public import Mathlib.Probability.ConditionalExpectation public import Mathlib.Probability.Kernel.Condexp /-! -# The conditional expectation kernel: freezing and independence +# The conditional expectation kernel: almost sure properties, freezing and independence + +A property that holds `μ`-almost everywhere holds, for almost every `ω`, almost everywhere under +the conditional expectation kernel at `ω`. If `Z` is measurable with respect to a sub-σ-algebra `m`, then integrating a function of `(Z, ω)` amounts to integrating out `ω` against the conditional expectation kernel with `Z` frozen: @@ -20,6 +23,8 @@ of the conditional expectation kernel by `X`, is almost surely the law of `X`. ## Main statements +* `LMLExplore.ae_trim_ae_condExpKernel`: a `μ`-almost everywhere property holds almost everywhere + under `condExpKernel μ m ω` for `μ.trim hm`-almost every `ω`. * `LMLExplore.lintegral_comp_condExpKernel`: the freezing lemma for nonnegative functions. * `LMLExplore.ae_trim_map_condExpKernel_eq_of_indep`: for `X` independent of `m`, `(condExpKernel μ m ω).map X = μ.map X` for almost every `ω`. @@ -40,6 +45,12 @@ namespace LMLExplore variable {Ω E : Type*} {m mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {mE : MeasurableSpace E} {μ : Measure Ω} [IsFiniteMeasure μ] +/-- A property that holds `μ`-almost everywhere holds, for `μ.trim hm`-almost every `ω`, almost +everywhere under the conditional expectation kernel at `ω`. -/ +lemma ae_trim_ae_condExpKernel (hm : m ≤ mΩ) {p : Ω → Prop} (h : ∀ᵐ ω ∂μ, p ω) : + ∀ᵐ ω ∂(μ.trim hm), ∀ᵐ ω' ∂(condExpKernel μ m ω), p ω' := + Measure.ae_ae_of_ae_comp (by rwa [condExpKernel_comp_trim hm]) + /-- **Freezing lemma for the conditional expectation kernel**: if `Z` is `m`-measurable, then for every measurable `Φ ≥ 0`, `∫⁻ ω, Φ (Z ω, ω) ∂μ = ∫⁻ ω, ∫⁻ ω', Φ (Z ω, ω') ∂(condExpKernel μ m ω) ∂μ`. -/ diff --git a/LMLExplore/Probability/Martingale/KLChernoff.lean b/LMLExplore/Probability/Martingale/KLChernoff.lean new file mode 100644 index 00000000..4a2e0c0c --- /dev/null +++ b/LMLExplore/Probability/Martingale/KLChernoff.lean @@ -0,0 +1,288 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LMLExplore.Probability.Martingale.RateFunction +public import LMLExplore.Probability.Moments.KLChernoff +import LMLExplore.MeasureTheory.Function.ConditionalExpectation.Real +import LMLExplore.Probability.Distributions.Bernoulli + +/-! +# Conditional Bernoulli domination and time-uniform Chernoff bounds in relative-entropy form + +A random variable `X` with values in `[0, 1]` whose conditional mean given a σ-algebra `m` is at +most `q` is *conditionally dominated above* by the Bernoulli law `Ber((1 : ℝ), 0, q)`: for +`t ≥ 0`, `E[exp (t X) | m] ≤ 1 - q + q exp t`, the moment generating function of that law +[GC11, Lemma 9; LS, Note 10.3.1]. The proof is the unconditional one +(`LMLExplore.mgfDominatedOn_Ici_bernoulliMeasure`, by convexity of `exp` on `[0, 1]`), applied to +the conditional law of `X` given `m`, the conditional expectation kernel. Symmetrically, if the +conditional mean is at least `q`, then `X` is conditionally dominated below by `Ber((1 : ℝ), 0, q)`, +for `t ≤ 0`. In the language of `LMLExplore.HasCondMGFBound`, the conditional moment generating +function of `X` is bounded by that of the Bernoulli law on `[0, ∞)` (resp. `(-∞, 0]`). + +Along a filtration `ℱ`, this applies to rewards `X k ∈ [0, 1]` that are `ℱ (k + 1)`-measurable +with conditional means given `ℱ k` at most (resp. at least) `m`, for instance the rewards of a +bandit algorithm whose arms have means at most (resp. at least) `m`, with no independence. The +self-normalized deviations of `LMLExplore.Probability.Martingale.RateFunction`, for the Bernoulli +law of mean `m`, whose rate function is the binary relative entropy `d(·, m)` on `[0, 1]` +(`LMLExplore.rateFunction_id_bernoulliMeasure`), then give [GC11, Theorem 10] for such rewards: +for selection indicators `w k ∈ {0, 1}` adapted to `ℱ`, `N t = ∑ k < t, w k` selected rewards +with mean `μ̂ t` after `t` rounds, `x > 0` and `n ≥ 2`, +`P(∃ t, 1 ≤ N t ≤ n, m < μ̂ t, x ≤ N t d(μ̂ t, m)) ≤ e ⌈x log n⌉ exp (-x)`, and the same below +`m`. Equivalently, the upper confidence level `U(μ̂ t, x / N t)` of the KL-UCB algorithm is below +`m` at some round with `1 ≤ N t ≤ n` with probability at most `e ⌈x log n⌉ exp (-x)` if the +conditional means are at least `m`, and the lower confidence level `L(μ̂ t, x / N t)` is above +`m` with the same probability if they are at most `m`. For `w k = 1` and independent rewards these +are the bounds of `LMLExplore.Probability.Moments.KLChernoff` on the first `s` variables. + +## Main statements + +* `LMLExplore.hasCondMGFBound_Ici_cgf_bernoulliMeasure`, + `LMLExplore.hasCondMGFBound_Iic_cgf_bernoulliMeasure`: [GC11, Lemma 9], a random variable with + values in `[0, 1]` and conditional mean at most (resp. at least) `q` has its conditional moment + generating function bounded by that of `Ber((1 : ℝ), 0, q)` on `Set.Ici 0` (resp. `Set.Iic 0`). +* `LMLExplore.measure_exists_gt_and_le_mul_klBer_le_of_condExp_le`, + `LMLExplore.measure_exists_lt_and_le_mul_klBer_le_of_le_condExp`: [GC11, Theorem 10] along a + filtration, the bound `e ⌈x log n⌉ exp (-x)` on the deviations of the selected means above + (resp. below) `m` measured by `d(·, m)`. +* `LMLExplore.measure_exists_klUpper_lt_le_of_le_condExp`, + `LMLExplore.measure_exists_lt_klLower_le_of_condExp_le`: the time-uniform coverage of the upper + (resp. lower) confidence levels along a filtration. + +## References + +* [GC11] A. Garivier and O. Cappé, *The KL-UCB algorithm for bounded stochastic bandits and + beyond*, COLT 2011, Lemma 9 and Theorem 10. +* T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020, + Note 10.3.1. +-/ + +public section + +open MeasureTheory InformationTheory ProbabilityTheory Filter Real Finset +open scoped ENNReal unitInterval + +namespace LMLExplore + +/-! ### Conditional domination by a Bernoulli law -/ + +section Domination + +variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] + {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → ℝ} + +/-- **Conditional domination above by a Bernoulli law** [GC11, Lemma 9]. If `X` is measurable with +values in `[0, 1]` almost surely and `E[X | m] ≤ q` almost surely, then the conditional moment +generating function of `X` given `m` is bounded by that of `Ber((1 : ℝ), 0, q)` on the nonnegative +parameters: `E[exp (t X) | m] ≤ 1 - q + q exp t` for `t ≥ 0`. -/ +theorem hasCondMGFBound_Ici_cgf_bernoulliMeasure (hX : Measurable X) + (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) {q : I} (hmean : μ[X | m] ≤ᵐ[μ] fun _ ↦ (q : ℝ)) : + HasCondMGFBound m hm X (cgf id Ber((1 : ℝ), 0, q)) (Set.Ici 0) μ := by + refine (hasCondMGFBound_cgf_of_ae_mgfDominatedOn + (fun _ _ ↦ integrable_exp_mul_of_mem_Icc hX.aemeasurable hX01) ?_).mono + (fun t ht ↦ ⟨ht, integrable_bernoulliMeasure (1 : ℝ) 0 q _⟩) fun _ _ ↦ le_rfl + -- the unconditional domination, under almost every conditional law + filter_upwards [ae_trim_ae_condExpKernel hm hX01, + condExp_ae_eq_trim_integral_condExpKernel hm (.of_mem_Icc 0 1 hX.aemeasurable hX01), + stronglyMeasurable_condExp.ae_le_trim_of_stronglyMeasurable hm stronglyMeasurable_const + hmean] with ω' h01 h_eq hq + exact mgfDominatedOn_Ici_bernoulliMeasure hX.aemeasurable h01 (h_eq ▸ hq) + +/-- **Conditional domination below by a Bernoulli law** [GC11, Lemma 9]. If `X` is measurable with +values in `[0, 1]` almost surely and `q ≤ E[X | m]` almost surely, then the conditional moment +generating function of `X` given `m` is bounded by that of `Ber((1 : ℝ), 0, q)` on the nonpositive +parameters: `E[exp (t X) | m] ≤ 1 - q + q exp t` for `t ≤ 0`. -/ +theorem hasCondMGFBound_Iic_cgf_bernoulliMeasure (hX : Measurable X) + (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) {q : I} (hmean : (fun _ ↦ (q : ℝ)) ≤ᵐ[μ] μ[X | m]) : + HasCondMGFBound m hm X (cgf id Ber((1 : ℝ), 0, q)) (Set.Iic 0) μ := by + refine (hasCondMGFBound_cgf_of_ae_mgfDominatedOn + (fun _ _ ↦ integrable_exp_mul_of_mem_Icc hX.aemeasurable hX01) ?_).mono + (fun t ht ↦ ⟨ht, integrable_bernoulliMeasure (1 : ℝ) 0 q _⟩) fun _ _ ↦ le_rfl + -- the unconditional domination, under almost every conditional law + filter_upwards [ae_trim_ae_condExpKernel hm hX01, + condExp_ae_eq_trim_integral_condExpKernel hm (.of_mem_Icc 0 1 hX.aemeasurable hX01), + stronglyMeasurable_const.ae_le_trim_of_stronglyMeasurable hm stronglyMeasurable_condExp + hmean] with ω' h01 h_eq hq + exact mgfDominatedOn_Iic_bernoulliMeasure hX.aemeasurable h01 (h_eq ▸ hq) + +end Domination + +/-! ### Self-normalized deviations along a filtration -/ + +section SelfNormalized + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {P : Measure Ω} + [IsProbabilityMeasure P] {ℱ : Filtration ℕ mΩ} {X w : ℕ → Ω → ℝ} {m : ℝ} + +/-- On a run of rewards in `[0, 1]` with selection indicators in `{0, 1}`, the mean of the +selected rewards lies in `[0, 1]` as soon as one is selected. -/ +private lemma mean_mem_Icc_of_one_le (hw01 : ∀ n ω, w n ω = 0 ∨ w n ω = 1) {ω : Ω} + (hω : ∀ k, X k ω ∈ Set.Icc 0 1) {t : ℕ} (ht : 1 ≤ ∑ k ∈ range t, w k ω) : + (∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω ∈ Set.Icc 0 1 := by + simpa only [centerMass, smul_eq_mul, inv_mul_eq_div] using (convex_Icc (0 : ℝ) 1).centerMass_mem + (fun k _ ↦ (hw01 k ω).elim (·.ge) fun h ↦ h ▸ zero_le_one) (zero_lt_one.trans_le ht) + fun k _ ↦ hω k + +omit [StandardBorelSpace Ω] [IsProbabilityMeasure P] in +/-- On the event where the rewards lie in `[0, 1]`, a deviation of the selected means from `q`, +in the direction given by the relation `r`, measured by `d(·, q)`, is a deviation from the mean +of `Ber((1 : ℝ), 0, q)` measured by the rate function of that law. So a bound on the probability +of the latter deviation bounds that of the former. -/ +private lemma measure_exists_le_mul_klBer_le_of_rateFunction (r : ℝ → ℝ → Prop) + (hX01 : ∀ n, ∀ᵐ ω ∂P, X n ω ∈ Set.Icc 0 1) (hw01 : ∀ n ω, w n ω = 0 ∨ w n ω = 1) {q : I} + {x : ℝ} {n : ℕ} {B : ℝ≥0∞} + (h : P {ω | ∃ t, 1 ≤ ∑ k ∈ range t, w k ω ∧ ∑ k ∈ range t, w k ω ≤ n ∧ + r (∫ y, id y ∂Ber((1 : ℝ), 0, q)) ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) ∧ + ENNReal.ofReal x ≤ ENNReal.ofReal (∑ k ∈ range t, w k ω) * + rateFunction id Ber((1 : ℝ), 0, q) + ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω)} ≤ B) : + P {ω | ∃ t, 1 ≤ ∑ k ∈ range t, w k ω ∧ ∑ k ∈ range t, w k ω ≤ n ∧ + r q ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) ∧ + ENNReal.ofReal x ≤ ENNReal.ofReal (∑ k ∈ range t, w k ω) * + klBer ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) q} ≤ B := by + refine (measure_mono_ae ?_).trans h + filter_upwards [ae_all_iff.2 hX01] with ω hω ⟨t, ht, htn, hr, hle⟩ + have h_mean : ∫ y, id y ∂Ber((1 : ℝ), 0, q) = q := + TauCeti.Probability.integral_id_bernoulliMeasure q + refine ⟨t, ht, htn, h_mean ▸ hr, ?_⟩ + rwa [rateFunction_id_bernoulliMeasure q (mean_mem_Icc_of_one_le hw01 hω ht)] + +/-- **Self-normalized deviations above the mean in relative-entropy form, along a filtration** +[GC11, Theorem 10]. Let `X k ∈ [0, 1]` be `ℱ (k + 1)`-measurable with `E[X k | ℱ k] ≤ m`, and let +the selection indicators `w` be adapted with values in `{0, 1}`. For `N t = ∑ k < t, w k` +selected variables with mean `μ̂ t` after `t` rounds, `x > 0` and `n ≥ 2`, the probability that +`1 ≤ N t ≤ n`, `m < μ̂ t` and `x ≤ N t d(μ̂ t, m)` at some round `t` is at most +`e ⌈x log n⌉ exp (-x)`, where `d` is the binary relative entropy. -/ +theorem measure_exists_gt_and_le_mul_klBer_le_of_condExp_le + (hX : ∀ n, Measurable[ℱ (n + 1)] (X n)) (hX01 : ∀ n, ∀ᵐ ω ∂P, X n ω ∈ Set.Icc 0 1) + (hmean : ∀ n, P[X n | ℱ n] ≤ᵐ[P] fun _ ↦ m) (hw : Adapted ℱ w) + (hw01 : ∀ n ω, w n ω = 0 ∨ w n ω = 1) {x : ℝ} (hx : 0 < x) {n : ℕ} (hn : 1 < n) : + P {ω | ∃ t, 1 ≤ ∑ k ∈ range t, w k ω ∧ ∑ k ∈ range t, w k ω ≤ n ∧ + m < (∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω ∧ + ENNReal.ofReal x ≤ ENNReal.ofReal (∑ k ∈ range t, w k ω) * + klBer ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) m} ≤ + ENNReal.ofReal (exp 1 * ⌈x * log n⌉₊ * exp (-x)) := by + have hXm n : Measurable (X n) := (hX n).mono (ℱ.le (n + 1)) le_rfl + have hX' : ∀ᵐ ω ∂P, ∀ k, X k ω ∈ Set.Icc 0 1 := ae_all_iff.2 hX01 + have hm0 : 0 ≤ m := le_of_ae_le_of_condExp_le (ℱ.le 0) (.of_mem_Icc 0 1 (hXm 0).aemeasurable + (hX01 0)) ((hX01 0).mono fun _ h ↦ h.1) (hmean 0) + rcases le_or_gt m 1 with hm1 | hm1 + swap + · -- for `m > 1`, no selected mean is above `m` + refine le_of_eq_of_le (measure_eq_zero_iff_ae_notMem.2 ?_) zero_le + filter_upwards [hX'] with ω hω ⟨t, ht, _, hlt, _⟩ + linarith [(mean_mem_Icc_of_one_le hw01 hω ht).2] + -- the variables are conditionally dominated above by the Bernoulli law of mean `m`, whose rate + -- function is `d(·, m)` on `[0, 1]` + exact measure_exists_le_mul_klBer_le_of_rateFunction (q := ⟨m, hm0, hm1⟩) (· < ·) hX01 hw01 + (measure_exists_gt_and_le_mul_rateFunction_le hX + (fun k ↦ (hasCondMGFBound_Ici_cgf_bernoulliMeasure (hXm k) (hX01 k) (hmean k)).mono + Set.inter_subset_left fun _ _ ↦ le_rfl) + hw hw01 (integrable_bernoulliMeasure (1 : ℝ) 0 _ id) hx hn) + +/-- **Self-normalized deviations below the mean in relative-entropy form, along a filtration** +[GC11, Theorem 10]. Let `X k ∈ [0, 1]` be `ℱ (k + 1)`-measurable with `m ≤ E[X k | ℱ k]`, and let +the selection indicators `w` be adapted with values in `{0, 1}`. For `N t = ∑ k < t, w k` +selected variables with mean `μ̂ t` after `t` rounds, `x > 0` and `n ≥ 2`, the probability that +`1 ≤ N t ≤ n`, `μ̂ t < m` and `x ≤ N t d(μ̂ t, m)` at some round `t` is at most +`e ⌈x log n⌉ exp (-x)`, where `d` is the binary relative entropy. -/ +theorem measure_exists_lt_and_le_mul_klBer_le_of_le_condExp + (hX : ∀ n, Measurable[ℱ (n + 1)] (X n)) (hX01 : ∀ n, ∀ᵐ ω ∂P, X n ω ∈ Set.Icc 0 1) + (hmean : ∀ n, (fun _ ↦ m) ≤ᵐ[P] P[X n | ℱ n]) (hw : Adapted ℱ w) + (hw01 : ∀ n ω, w n ω = 0 ∨ w n ω = 1) {x : ℝ} (hx : 0 < x) {n : ℕ} (hn : 1 < n) : + P {ω | ∃ t, 1 ≤ ∑ k ∈ range t, w k ω ∧ ∑ k ∈ range t, w k ω ≤ n ∧ + (∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω < m ∧ + ENNReal.ofReal x ≤ ENNReal.ofReal (∑ k ∈ range t, w k ω) * + klBer ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) m} ≤ + ENNReal.ofReal (exp 1 * ⌈x * log n⌉₊ * exp (-x)) := by + have hXm n : Measurable (X n) := (hX n).mono (ℱ.le (n + 1)) le_rfl + have hX' : ∀ᵐ ω ∂P, ∀ k, X k ω ∈ Set.Icc 0 1 := ae_all_iff.2 hX01 + have hm1 : m ≤ 1 := le_of_le_condExp_of_ae_le (ℱ.le 0) (.of_mem_Icc 0 1 (hXm 0).aemeasurable + (hX01 0)) (hmean 0) ((hX01 0).mono fun _ h ↦ h.2) + rcases le_or_gt 0 m with hm0 | hm0 + swap + · -- for `m < 0`, no selected mean is below `m` + refine le_of_eq_of_le (measure_eq_zero_iff_ae_notMem.2 ?_) zero_le + filter_upwards [hX'] with ω hω ⟨t, ht, _, hlt, _⟩ + linarith [(mean_mem_Icc_of_one_le hw01 hω ht).1] + -- the variables are conditionally dominated below by the Bernoulli law of mean `m`, whose rate + -- function is `d(·, m)` on `[0, 1]` + exact measure_exists_le_mul_klBer_le_of_rateFunction (q := ⟨m, hm0, hm1⟩) (fun a b ↦ b < a) hX01 + hw01 (measure_exists_lt_and_le_mul_rateFunction_le hX + (fun k ↦ (hasCondMGFBound_Iic_cgf_bernoulliMeasure (hXm k) (hX01 k) (hmean k)).mono + Set.inter_subset_left fun _ _ ↦ le_rfl) + hw hw01 (integrable_bernoulliMeasure (1 : ℝ) 0 _ id) hx hn) + +/-- `x = N * (x / N)` in `ℝ≥0∞` for a positive real `N`. -/ +private lemma ofReal_eq_ofReal_mul_ofReal_div {x N : ℝ} (hN : 0 < N) : + ENNReal.ofReal x = ENNReal.ofReal N * ENNReal.ofReal (x / N) := by + rw [← ENNReal.ofReal_mul hN.le, mul_div_cancel₀ x hN.ne'] + +/-- **Time-uniform coverage of the upper confidence level, along a filtration** +[GC11, Theorem 10]. Let `X k ∈ [0, 1]` be `ℱ (k + 1)`-measurable with `m ≤ E[X k | ℱ k]`, and let +the selection indicators `w` be adapted with values in `{0, 1}`. For `N t = ∑ k < t, w k` +selected variables with mean `μ̂ t` after `t` rounds, `x > 0` and `n ≥ 2`, the probability that +`1 ≤ N t ≤ n` and the upper confidence level `U(μ̂ t, x / N t)` is less than `m` at some round +`t` is at most `e ⌈x log n⌉ exp (-x)`. -/ +theorem measure_exists_klUpper_lt_le_of_le_condExp + (hX : ∀ n, Measurable[ℱ (n + 1)] (X n)) (hX01 : ∀ n, ∀ᵐ ω ∂P, X n ω ∈ Set.Icc 0 1) + (hmean : ∀ n, (fun _ ↦ m) ≤ᵐ[P] P[X n | ℱ n]) (hw : Adapted ℱ w) + (hw01 : ∀ n ω, w n ω = 0 ∨ w n ω = 1) {x : ℝ} (hx : 0 < x) {n : ℕ} (hn : 1 < n) : + P {ω | ∃ t, 1 ≤ ∑ k ∈ range t, w k ω ∧ ∑ k ∈ range t, w k ω ≤ n ∧ + klUpper ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) + (ENNReal.ofReal (x / ∑ k ∈ range t, w k ω)) < m} ≤ + ENNReal.ofReal (exp 1 * ⌈x * log n⌉₊ * exp (-x)) := by + refine (measure_mono_ae ?_).trans + (measure_exists_lt_and_le_mul_klBer_le_of_le_condExp hX hX01 hmean hw hw01 hx hn) + filter_upwards [ae_all_iff.2 hX01] with ω hω ⟨t, ht, htn, hU⟩ + -- `μ̂ ≤ U(μ̂, x / N) < m`, and `m ≤ U(μ̂, x / N)` unless `x / N < d(μ̂, m)` + have hp := mean_mem_Icc_of_one_le hw01 hω ht + have hpU := (klUpper_mem_Icc hp.2 (ENNReal.ofReal (x / ∑ k ∈ range t, w k ω))).1 + have hm1 : m ≤ 1 := le_of_le_condExp_of_ae_le (ℱ.le 0) + (.of_mem_Icc 0 1 ((hX 0).mono (ℱ.le 1) le_rfl).aemeasurable (hX01 0)) (hmean 0) + ((hX01 0).mono fun _ h ↦ h.2) + have hd : ENNReal.ofReal (x / ∑ k ∈ range t, w k ω) < + klBer ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) m := by + by_contra! h + exact hU.not_ge ((le_klUpper_iff ⟨hpU.trans hU.le, hm1⟩).2 h) + refine ⟨t, ht, htn, hpU.trans_lt hU, ?_⟩ + rw [ofReal_eq_ofReal_mul_ofReal_div (zero_lt_one.trans_le ht)] + gcongr + +/-- **Time-uniform coverage of the lower confidence level, along a filtration** +[GC11, Theorem 10]. Let `X k ∈ [0, 1]` be `ℱ (k + 1)`-measurable with `E[X k | ℱ k] ≤ m`, and let +the selection indicators `w` be adapted with values in `{0, 1}`. For `N t = ∑ k < t, w k` +selected variables with mean `μ̂ t` after `t` rounds, `x > 0` and `n ≥ 2`, the probability that +`1 ≤ N t ≤ n` and the lower confidence level `L(μ̂ t, x / N t)` is more than `m` at some round +`t` is at most `e ⌈x log n⌉ exp (-x)`. -/ +theorem measure_exists_lt_klLower_le_of_condExp_le + (hX : ∀ n, Measurable[ℱ (n + 1)] (X n)) (hX01 : ∀ n, ∀ᵐ ω ∂P, X n ω ∈ Set.Icc 0 1) + (hmean : ∀ n, P[X n | ℱ n] ≤ᵐ[P] fun _ ↦ m) (hw : Adapted ℱ w) + (hw01 : ∀ n ω, w n ω = 0 ∨ w n ω = 1) {x : ℝ} (hx : 0 < x) {n : ℕ} (hn : 1 < n) : + P {ω | ∃ t, 1 ≤ ∑ k ∈ range t, w k ω ∧ ∑ k ∈ range t, w k ω ≤ n ∧ + m < klLower ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) + (ENNReal.ofReal (x / ∑ k ∈ range t, w k ω))} ≤ + ENNReal.ofReal (exp 1 * ⌈x * log n⌉₊ * exp (-x)) := by + refine (measure_mono_ae ?_).trans + (measure_exists_gt_and_le_mul_klBer_le_of_condExp_le hX hX01 hmean hw hw01 hx hn) + filter_upwards [ae_all_iff.2 hX01] with ω hω ⟨t, ht, htn, hL⟩ + -- `m < L(μ̂, x / N) ≤ μ̂`, and `L(μ̂, x / N) ≤ m` unless `x / N < d(μ̂, m)` + have hp := mean_mem_Icc_of_one_le hw01 hω ht + have hLp := klLower_mem_Icc hp.1 (ENNReal.ofReal (x / ∑ k ∈ range t, w k ω)) + have hm0 : 0 ≤ m := le_of_ae_le_of_condExp_le (ℱ.le 0) + (.of_mem_Icc 0 1 ((hX 0).mono (ℱ.le 1) le_rfl).aemeasurable (hX01 0)) + ((hX01 0).mono fun _ h ↦ h.1) (hmean 0) + have hd : ENNReal.ofReal (x / ∑ k ∈ range t, w k ω) < + klBer ((∑ k ∈ range t, w k ω * X k ω) / ∑ k ∈ range t, w k ω) m := by + by_contra! h + exact hL.not_ge ((klLower_le_iff ⟨hm0, hL.le.trans hLp.2⟩).2 h) + refine ⟨t, ht, htn, hL.trans_le hLp.2, ?_⟩ + rw [ofReal_eq_ofReal_mul_ofReal_div (zero_lt_one.trans_le ht)] + gcongr + +end SelfNormalized + +end LMLExplore diff --git a/LMLExplore/Probability/Moments/MGF/Bound.lean b/LMLExplore/Probability/Moments/MGF/Bound.lean index b19c5aa0..684b8d85 100644 --- a/LMLExplore/Probability/Moments/MGF/Bound.lean +++ b/LMLExplore/Probability/Moments/MGF/Bound.lean @@ -65,6 +65,8 @@ weights of an exponential supermartingale. `LMLExplore.hasMGFBound_iff_hasSubexponentialMGF`). * `LMLExplore.mgfDominatedOn_iff_hasMGFBound`: domination by `Y` on `Λ` is the bound by the cumulant generating function of `Y` on `Λ`. +* `LMLExplore.hasCondMGFBound_cgf_of_ae_mgfDominatedOn`: domination by `Y` on `Λ` under almost + every conditional law gives the conditional bound by the cumulant generating function of `Y`. * `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`. @@ -417,6 +419,31 @@ lemma _root_.ProbabilityTheory.HasSubgaussianMGF.mgfDominatedOn_gaussianReal {a end Unconditional +section Dominated + +variable {Ω Ω' : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] + {mΩ' : MeasurableSpace Ω'} {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → ℝ} {Λ : Set ℝ} + {Q : Measure Ω'} [NeZero Q] {Y : Ω' → ℝ} + +/-- **Domination under the conditional expectation kernel.** If `exp (t * X)` is `μ`-integrable +for every `t ∈ Λ` at which `exp (t * Y)` is `Q`-integrable, and for almost every `ω'`, `X` under +the conditional expectation kernel at `ω'` is dominated by `Y` under `Q` on `Λ`, then the +conditional moment generating function of `X` given `m` is bounded by `exp (cgf Y Q)` on these +parameters. -/ +lemma hasCondMGFBound_cgf_of_ae_mgfDominatedOn + (hX : ∀ t ∈ Λ ∩ integrableExpSet Y Q, Integrable (fun ω ↦ exp (t * X ω)) μ) + (h : ∀ᵐ ω' ∂(μ.trim hm), MGFDominatedOn X (condExpKernel μ m ω') Y Q Λ) : + HasCondMGFBound m hm X (cgf Y Q) (Λ ∩ integrableExpSet Y Q) μ := by + refine hasCondMGFBound_iff_kernel.2 ⟨fun t ht ↦ ?_, ?_, ?_⟩ + · rw [condExpKernel_comp_trim hm] + exact hX t ht + · filter_upwards [h] with ω' h t ht + exact (mgfDominatedOn_iff_hasMGFBound.1 h).integrable_exp_mul ht + · filter_upwards [h] with ω' h t ht + exact (mgfDominatedOn_iff_hasMGFBound.1 h).mgf_le ht + +end Dominated + section Indep variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω]