From 0f8bcc49c3b7c0709329807dea22355dd974e6ea Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 20:57:55 +0100 Subject: [PATCH 1/2] feat: conditional Bernoulli domination of [0, 1]-valued variables and GC11 Theorem 10 along a filtration MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A variable with values in [0, 1] whose conditional mean is at most (at least) q has its conditional moment generating function bounded by that of Ber(q) on [0, ∞) (on (-∞, 0]) [GC11, Lemma 9]. Along a filtration this gives the self-normalized deviations in relative-entropy form and the time-uniform coverage of the KL-UCB confidence levels for selected rewards with bounded conditional means. Co-Authored-By: Claude Code Co-Authored-By: Claude Opus 5.5 --- .../Probability/Martingale/KLChernoff.lean | 317 ++++++++++++++++++ 1 file changed, 317 insertions(+) create mode 100644 LMLExplore/Probability/Martingale/KLChernoff.lean diff --git a/LMLExplore/Probability/Martingale/KLChernoff.lean b/LMLExplore/Probability/Martingale/KLChernoff.lean new file mode 100644 index 00000000..e8c90f9b --- /dev/null +++ b/LMLExplore/Probability/Martingale/KLChernoff.lean @@ -0,0 +1,317 @@ +/- +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.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 : Ω → ℝ} + +/-- If `X ∈ [0, 1]` almost surely, then for almost every `ω'` (for the restriction of `μ` to `m`), +`X ∈ [0, 1]` almost surely under the conditional expectation kernel at `ω'`, and the mean of `X` +under that kernel is `E[X | m] ω'`. -/ +private lemma ae_trim_ae_mem_Icc_and_condExp_eq (hm : m ≤ mΩ) (hX : Measurable X) + (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) : + ∀ᵐ ω' ∂(μ.trim hm), (∀ᵐ ω ∂(condExpKernel μ m ω'), X ω ∈ Set.Icc 0 1) ∧ + μ[X | m] ω' = ∫ ω, X ω ∂(condExpKernel μ m ω') := by + have h01 : ∀ᵐ ω' ∂(μ.trim hm), ∀ᵐ ω ∂(condExpKernel μ m ω'), X ω ∈ Set.Icc 0 1 := + Measure.ae_ae_of_ae_comp (by rwa [condExpKernel_comp_trim hm]) + filter_upwards [h01, condExp_ae_eq_trim_integral_condExpKernel hm + (.of_mem_Icc 0 1 hX.aemeasurable hX01)] with ω' h01 h_eq using ⟨h01, h_eq⟩ + +/-- **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 + have hmean' := stronglyMeasurable_condExp.ae_le_trim_of_stronglyMeasurable hm + stronglyMeasurable_const hmean + refine hasCondMGFBound_iff_kernel.2 ⟨fun t _ ↦ ?_, ?_, ?_⟩ + · rw [condExpKernel_comp_trim hm] + exact integrable_exp_mul_of_mem_Icc hX.aemeasurable hX01 + · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01] with ω' h t _ + exact integrable_exp_mul_of_mem_Icc hX.aemeasurable h.1 + · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01, hmean'] with ω' h hq t ht + have h_int := integrable_bernoulliMeasure (1 : ℝ) 0 q fun y ↦ exp (t * id y) + rw [exp_cgf h_int] + exact (mgfDominatedOn_Ici_bernoulliMeasure hX.aemeasurable h.1 (h.2 ▸ hq)).mgf_le ht h_int + +/-- **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 + have hmean' := stronglyMeasurable_const.ae_le_trim_of_stronglyMeasurable hm + stronglyMeasurable_condExp hmean + refine hasCondMGFBound_iff_kernel.2 ⟨fun t _ ↦ ?_, ?_, ?_⟩ + · rw [condExpKernel_comp_trim hm] + exact integrable_exp_mul_of_mem_Icc hX.aemeasurable hX01 + · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01] with ω' h t _ + exact integrable_exp_mul_of_mem_Icc hX.aemeasurable h.1 + · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01, hmean'] with ω' h hq t ht + have h_int := integrable_bernoulliMeasure (1 : ℝ) 0 q fun y ↦ exp (t * id y) + rw [exp_cgf h_int] + exact (mgfDominatedOn_Iic_bernoulliMeasure hX.aemeasurable h.1 (h.2 ▸ hq)).mgf_le ht h_int + +end Domination + +section CondExpBounds + +variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] + {X : Ω → ℝ} {c : ℝ} + +/-- A bound `E[X | m] ≤ c` on the conditional mean of a variable `X ∈ [0, 1]` forces `0 ≤ c`. -/ +private lemma nonneg_of_condExp_le (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) + (hmean : μ[X | m] ≤ᵐ[μ] fun _ ↦ c) : 0 ≤ c := by + obtain ⟨ω, h0, hc⟩ := ((condExp_nonneg (hX01.mono fun ω hω ↦ hω.1)).and hmean).exists + exact h0.trans hc + +/-- A bound `c ≤ E[X | m]` on the conditional mean of a variable `X ∈ [0, 1]`, for a +sub-σ-algebra `m`, forces `c ≤ 1`. -/ +private lemma le_one_of_le_condExp (hm : m ≤ mΩ) (hX : Measurable X) + (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) (hmean : (fun _ ↦ c) ≤ᵐ[μ] μ[X | m]) : c ≤ 1 := by + have h_le : μ[X | m] ≤ᵐ[μ] fun _ ↦ (1 : ℝ) := by + have := condExp_mono (m := m) (.of_mem_Icc 0 1 hX.aemeasurable hX01) + (integrable_const (1 : ℝ)) (hX01.mono fun ω hω ↦ hω.2) + rwa [condExp_const hm] at this + obtain ⟨ω, hc, h1⟩ := (hmean.and h_le).exists + exact hc.trans h1 + +end CondExpBounds + +/-! ### Self-normalized deviations along a filtration -/ + +section SelfNormalized + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {P : Measure Ω} + [IsProbabilityMeasure P] {ℱ : Filtration ℕ mΩ} {X w : ℕ → Ω → ℝ} {m : ℝ} + +/-- The mean `(∑ k < t, w k x k) / ∑ k < t, w k` of numbers `x k ∈ [0, 1]` with nonnegative +weights of positive sum lies in `[0, 1]`. -/ +private lemma sum_mul_div_sum_mem_Icc {w x : ℕ → ℝ} (hw : ∀ k, 0 ≤ w k) + (hx : ∀ k, x k ∈ Set.Icc 0 1) {t : ℕ} (ht : 0 < ∑ k ∈ range t, w k) : + (∑ k ∈ range t, w k * x k) / ∑ k ∈ range t, w k ∈ Set.Icc 0 1 := + ⟨div_nonneg (sum_nonneg fun k _ ↦ mul_nonneg (hw k) (hx k).1) ht.le, + (div_le_one ht).2 (sum_le_sum fun k _ ↦ mul_le_of_le_one_right (hw k) (hx k).2)⟩ + +/-- 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 := + sum_mul_div_sum_mem_Icc (fun k ↦ (hw01 k ω).elim (·.ge) fun h ↦ h ▸ zero_le_one) hω + (zero_lt_one.trans_le 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 := nonneg_of_condExp_le (hX01 0) (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]` + set q : I := ⟨m, hm0, hm1⟩ + have h := measure_exists_gt_and_le_mul_rateFunction_le hX + (fun k ↦ (hasCondMGFBound_Ici_cgf_bernoulliMeasure (q := q) (hXm k) (hX01 k) + (hmean k)).mono Set.inter_subset_left fun _ _ ↦ le_rfl) + hw hw01 (integrable_bernoulliMeasure (1 : ℝ) 0 q id) hx hn + refine (measure_mono_ae ?_).trans h + filter_upwards [hX'] with ω hω ⟨t, ht, htn, hlt, hle⟩ + have h_mean : ∫ y, id y ∂Ber((1 : ℝ), 0, q) = m := + TauCeti.Probability.integral_id_bernoulliMeasure q + refine ⟨t, ht, htn, h_mean ▸ hlt, ?_⟩ + rwa [rateFunction_id_bernoulliMeasure q (mean_mem_Icc_of_one_le hw01 hω ht)] + +/-- **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_one_of_le_condExp (ℱ.le 0) (hXm 0) (hX01 0) (hmean 0) + 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]` + set q : I := ⟨m, hm0, hm1⟩ + have h := measure_exists_lt_and_le_mul_rateFunction_le hX + (fun k ↦ (hasCondMGFBound_Iic_cgf_bernoulliMeasure (q := q) (hXm k) (hX01 k) + (hmean k)).mono Set.inter_subset_left fun _ _ ↦ le_rfl) + hw hw01 (integrable_bernoulliMeasure (1 : ℝ) 0 q id) hx hn + refine (measure_mono_ae ?_).trans h + filter_upwards [hX'] with ω hω ⟨t, ht, htn, hlt, hle⟩ + have h_mean : ∫ y, id y ∂Ber((1 : ℝ), 0, q) = m := + TauCeti.Probability.integral_id_bernoulliMeasure q + refine ⟨t, ht, htn, h_mean ▸ hlt, ?_⟩ + rwa [rateFunction_id_bernoulliMeasure q (mean_mem_Icc_of_one_le hw01 hω ht)] + +/-- `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_one_of_le_condExp (ℱ.le 0) ((hX 0).mono (ℱ.le 1) le_rfl) (hX01 0) (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 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 := nonneg_of_condExp_le (hX01 0) (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 From b48ebdc6d2ba139bd7907f99bc3491aabfcf54f8 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 21:25:20 +0100 Subject: [PATCH 2/2] refactor: expose the general conditional lemmas and factor the Bernoulli proofs Address the api-design and proof-quality review findings: - add `hasCondMGFBound_cgf_of_ae_mgfDominatedOn` (MGF/Bound): domination under almost every conditional law gives the conditional bound by the cgf, and derive both conditional Bernoulli dominations from it; - add `ae_trim_ae_condExpKernel` (Kernel/Condexp) and use Mathlib's `condExp_ae_eq_trim_integral_condExpKernel` for the mean identity, removing the private `ae_trim_ae_mem_Icc_and_condExp_eq`; - replace the private `nonneg_of_condExp_le` / `le_one_of_le_condExp` by the general public `le_of_ae_le_of_condExp_le` / `le_of_le_condExp_of_ae_le` (MeasureTheory/Function/ConditionalExpectation/Real); - replace the private `sum_mul_div_sum_mem_Icc` by Mathlib's `Convex.centerMass_mem`; - factor the shared tail of the two filtration theorems into one helper. Co-Authored-By: Claude Code --- .../Function/ConditionalExpectation/Real.lean | 55 ++++++ LMLExplore/Probability/Kernel/Condexp.lean | 13 +- .../Probability/Martingale/KLChernoff.lean | 163 +++++++----------- LMLExplore/Probability/Moments/MGF/Bound.lean | 27 +++ 4 files changed, 161 insertions(+), 97 deletions(-) create mode 100644 LMLExplore/MeasureTheory/Function/ConditionalExpectation/Real.lean 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 index e8c90f9b..4a2e0c0c 100644 --- a/LMLExplore/Probability/Martingale/KLChernoff.lean +++ b/LMLExplore/Probability/Martingale/KLChernoff.lean @@ -7,6 +7,7 @@ module public import LMLExplore.Probability.Martingale.RateFunction public import LMLExplore.Probability.Moments.KLChernoff +import LMLExplore.MeasureTheory.Function.ConditionalExpectation.Real import LMLExplore.Probability.Distributions.Bernoulli /-! @@ -73,18 +74,6 @@ section Domination variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → ℝ} -/-- If `X ∈ [0, 1]` almost surely, then for almost every `ω'` (for the restriction of `μ` to `m`), -`X ∈ [0, 1]` almost surely under the conditional expectation kernel at `ω'`, and the mean of `X` -under that kernel is `E[X | m] ω'`. -/ -private lemma ae_trim_ae_mem_Icc_and_condExp_eq (hm : m ≤ mΩ) (hX : Measurable X) - (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) : - ∀ᵐ ω' ∂(μ.trim hm), (∀ᵐ ω ∂(condExpKernel μ m ω'), X ω ∈ Set.Icc 0 1) ∧ - μ[X | m] ω' = ∫ ω, X ω ∂(condExpKernel μ m ω') := by - have h01 : ∀ᵐ ω' ∂(μ.trim hm), ∀ᵐ ω ∂(condExpKernel μ m ω'), X ω ∈ Set.Icc 0 1 := - Measure.ae_ae_of_ae_comp (by rwa [condExpKernel_comp_trim hm]) - filter_upwards [h01, condExp_ae_eq_trim_integral_condExpKernel hm - (.of_mem_Icc 0 1 hX.aemeasurable hX01)] with ω' h01 h_eq using ⟨h01, h_eq⟩ - /-- **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 @@ -92,17 +81,15 @@ 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 - have hmean' := stronglyMeasurable_condExp.ae_le_trim_of_stronglyMeasurable hm - stronglyMeasurable_const hmean - refine hasCondMGFBound_iff_kernel.2 ⟨fun t _ ↦ ?_, ?_, ?_⟩ - · rw [condExpKernel_comp_trim hm] - exact integrable_exp_mul_of_mem_Icc hX.aemeasurable hX01 - · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01] with ω' h t _ - exact integrable_exp_mul_of_mem_Icc hX.aemeasurable h.1 - · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01, hmean'] with ω' h hq t ht - have h_int := integrable_bernoulliMeasure (1 : ℝ) 0 q fun y ↦ exp (t * id y) - rw [exp_cgf h_int] - exact (mgfDominatedOn_Ici_bernoulliMeasure hX.aemeasurable h.1 (h.2 ▸ hq)).mgf_le ht h_int + 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 @@ -111,44 +98,18 @@ 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 - have hmean' := stronglyMeasurable_const.ae_le_trim_of_stronglyMeasurable hm - stronglyMeasurable_condExp hmean - refine hasCondMGFBound_iff_kernel.2 ⟨fun t _ ↦ ?_, ?_, ?_⟩ - · rw [condExpKernel_comp_trim hm] - exact integrable_exp_mul_of_mem_Icc hX.aemeasurable hX01 - · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01] with ω' h t _ - exact integrable_exp_mul_of_mem_Icc hX.aemeasurable h.1 - · filter_upwards [ae_trim_ae_mem_Icc_and_condExp_eq hm hX hX01, hmean'] with ω' h hq t ht - have h_int := integrable_bernoulliMeasure (1 : ℝ) 0 q fun y ↦ exp (t * id y) - rw [exp_cgf h_int] - exact (mgfDominatedOn_Iic_bernoulliMeasure hX.aemeasurable h.1 (h.2 ▸ hq)).mgf_le ht h_int + 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 -section CondExpBounds - -variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ] - {X : Ω → ℝ} {c : ℝ} - -/-- A bound `E[X | m] ≤ c` on the conditional mean of a variable `X ∈ [0, 1]` forces `0 ≤ c`. -/ -private lemma nonneg_of_condExp_le (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) - (hmean : μ[X | m] ≤ᵐ[μ] fun _ ↦ c) : 0 ≤ c := by - obtain ⟨ω, h0, hc⟩ := ((condExp_nonneg (hX01.mono fun ω hω ↦ hω.1)).and hmean).exists - exact h0.trans hc - -/-- A bound `c ≤ E[X | m]` on the conditional mean of a variable `X ∈ [0, 1]`, for a -sub-σ-algebra `m`, forces `c ≤ 1`. -/ -private lemma le_one_of_le_condExp (hm : m ≤ mΩ) (hX : Measurable X) - (hX01 : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc 0 1) (hmean : (fun _ ↦ c) ≤ᵐ[μ] μ[X | m]) : c ≤ 1 := by - have h_le : μ[X | m] ≤ᵐ[μ] fun _ ↦ (1 : ℝ) := by - have := condExp_mono (m := m) (.of_mem_Icc 0 1 hX.aemeasurable hX01) - (integrable_const (1 : ℝ)) (hX01.mono fun ω hω ↦ hω.2) - rwa [condExp_const hm] at this - obtain ⟨ω, hc, h1⟩ := (hmean.and h_le).exists - exact hc.trans h1 - -end CondExpBounds - /-! ### Self-normalized deviations along a filtration -/ section SelfNormalized @@ -156,21 +117,38 @@ section SelfNormalized variable {Ω : Type*} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {ℱ : Filtration ℕ mΩ} {X w : ℕ → Ω → ℝ} {m : ℝ} -/-- The mean `(∑ k < t, w k x k) / ∑ k < t, w k` of numbers `x k ∈ [0, 1]` with nonnegative -weights of positive sum lies in `[0, 1]`. -/ -private lemma sum_mul_div_sum_mem_Icc {w x : ℕ → ℝ} (hw : ∀ k, 0 ≤ w k) - (hx : ∀ k, x k ∈ Set.Icc 0 1) {t : ℕ} (ht : 0 < ∑ k ∈ range t, w k) : - (∑ k ∈ range t, w k * x k) / ∑ k ∈ range t, w k ∈ Set.Icc 0 1 := - ⟨div_nonneg (sum_nonneg fun k _ ↦ mul_nonneg (hw k) (hx k).1) ht.le, - (div_le_one ht).2 (sum_le_sum fun k _ ↦ mul_le_of_le_one_right (hw k) (hx k).2)⟩ - /-- 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 := - sum_mul_div_sum_mem_Icc (fun k ↦ (hw01 k ω).elim (·.ge) fun h ↦ h ▸ zero_le_one) hω - (zero_lt_one.trans_le ht) + (∑ 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 @@ -189,7 +167,8 @@ theorem measure_exists_gt_and_le_mul_klBer_le_of_condExp_le 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 := nonneg_of_condExp_le (hX01 0) (hmean 0) + 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` @@ -198,17 +177,11 @@ theorem measure_exists_gt_and_le_mul_klBer_le_of_condExp_le 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]` - set q : I := ⟨m, hm0, hm1⟩ - have h := measure_exists_gt_and_le_mul_rateFunction_le hX - (fun k ↦ (hasCondMGFBound_Ici_cgf_bernoulliMeasure (q := q) (hXm k) (hX01 k) - (hmean k)).mono Set.inter_subset_left fun _ _ ↦ le_rfl) - hw hw01 (integrable_bernoulliMeasure (1 : ℝ) 0 q id) hx hn - refine (measure_mono_ae ?_).trans h - filter_upwards [hX'] with ω hω ⟨t, ht, htn, hlt, hle⟩ - have h_mean : ∫ y, id y ∂Ber((1 : ℝ), 0, q) = m := - TauCeti.Probability.integral_id_bernoulliMeasure q - refine ⟨t, ht, htn, h_mean ▸ hlt, ?_⟩ - rwa [rateFunction_id_bernoulliMeasure q (mean_mem_Icc_of_one_le hw01 hω ht)] + 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 @@ -227,7 +200,8 @@ theorem measure_exists_lt_and_le_mul_klBer_le_of_le_condExp 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_one_of_le_condExp (ℱ.le 0) (hXm 0) (hX01 0) (hmean 0) + 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` @@ -236,17 +210,11 @@ theorem measure_exists_lt_and_le_mul_klBer_le_of_le_condExp 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]` - set q : I := ⟨m, hm0, hm1⟩ - have h := measure_exists_lt_and_le_mul_rateFunction_le hX - (fun k ↦ (hasCondMGFBound_Iic_cgf_bernoulliMeasure (q := q) (hXm k) (hX01 k) - (hmean k)).mono Set.inter_subset_left fun _ _ ↦ le_rfl) - hw hw01 (integrable_bernoulliMeasure (1 : ℝ) 0 q id) hx hn - refine (measure_mono_ae ?_).trans h - filter_upwards [hX'] with ω hω ⟨t, ht, htn, hlt, hle⟩ - have h_mean : ∫ y, id y ∂Ber((1 : ℝ), 0, q) = m := - TauCeti.Probability.integral_id_bernoulliMeasure q - refine ⟨t, ht, htn, h_mean ▸ hlt, ?_⟩ - rwa [rateFunction_id_bernoulliMeasure q (mean_mem_Icc_of_one_le hw01 hω ht)] + 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) : @@ -273,8 +241,9 @@ theorem measure_exists_klUpper_lt_le_of_le_condExp -- `μ̂ ≤ 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_one_of_le_condExp (ℱ.le 0) ((hX 0).mono (ℱ.le 1) le_rfl) (hX01 0) (hmean 0) + 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 @@ -303,7 +272,9 @@ theorem measure_exists_lt_klLower_le_of_condExp_le -- `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 := nonneg_of_condExp_le (hX01 0) (hmean 0) + 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 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 Ω]