From 31e7fa018c469ffeff4bb078cec891899a34c76e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:37:49 +0100 Subject: [PATCH 1/2] feat: a composite strong law of large numbers under bounded centred first moments MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For a set of integrable laws on ℝ with centred first absolute moments at most c, for every α > 0 some stopping time of Filtration.piLE is finite on every sequence whose sample means do not converge and finite with probability at most α under i.i.d. sampling from each law: the stopping-time form of the composite strong law of EValues, Layer 3, item 5. On the way: Doob's upcrossing inequality with the initial term, and maximal and upcrossing inequalities for the sample means of an exchangeable sequence, from the reverse martingale of the sample means. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- LMLExplore/EValues/CompositeStrongLaw.lean | 258 ++++++++++++++++ .../Probability/Martingale/SampleMean.lean | 285 ++++++++++++++++++ .../Probability/Martingale/Upcrossing.lean | 85 ++++++ 3 files changed, 628 insertions(+) create mode 100644 LMLExplore/EValues/CompositeStrongLaw.lean create mode 100644 LMLExplore/Probability/Martingale/SampleMean.lean create mode 100644 LMLExplore/Probability/Martingale/Upcrossing.lean diff --git a/LMLExplore/EValues/CompositeStrongLaw.lean b/LMLExplore/EValues/CompositeStrongLaw.lean new file mode 100644 index 00000000..6adbce82 --- /dev/null +++ b/LMLExplore/EValues/CompositeStrongLaw.lean @@ -0,0 +1,258 @@ +/- +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.Probability.ProductMeasure +public import Mathlib.Probability.Process.Stopping +import LMLExplore.Probability.Martingale.SampleMean +import LMLExplore.Probability.Martingale.Upcrossing +import Mathlib.Probability.Martingale.Convergence +import Mathlib.Probability.Process.HittingTime +import Statlib.ForMathlib.Probability.Process.Filtration +import Statlib.ForMathlib.Probability.ProductMeasure +import TauCeti.Probability.Exchangeability.PathSpace.Law.Basic + +/-! +# A composite strong law of large numbers + +For a set `𝒫` of laws of a sequence of observations, the inverse capital outer measure of a set +`A` of sequences is the infimum of `sup_{P ∈ 𝒫} P (τ < ∞)` over the stopping times `τ` that are +finite on `A` [RLKR23]. It is zero exactly when, for every `α > 0`, some stopping time is finite +on `A` and finite with probability at most `α` under every member of `𝒫`, and exactly when some +e-process for `𝒫` tends to infinity on `A` [RLKR23, Theorem 3.1]. A composite strong law of large +numbers says that the set of the sequences whose sample means do not converge has inverse capital +outer measure zero for a null of i.i.d. laws. + +This file proves it for the i.i.d. laws on `ℕ → ℝ` whose marginal ranges over a set of integrable +laws `P` with centred first absolute moments `∫ |x - m_P| dP ≤ c` for one constant `c`, where +`m_P` is the mean of `P`, in the stopping-time form, for the canonical filtration +`Filtration.piLE`. The centred uniform integrability under which [RLKR23, §4.2] proves a composite +strong law implies this hypothesis. + +## Main statements + +* `ProbabilityTheory.exists_isStoppingTime_lt_top_of_not_tendsto_mean`: the composite strong law. + +## Implementation notes + +The stopping time stops at the first time `n` at which, for some interval `[a, b]` with rational +endpoints, the sample means `X̄₁, …, X̄ₙ₊₁` have completed `K (a, b)` upcrossings of `[a, b]`, or +at which `X̄ₙ₊₁` is at distance at least `2 L` from the first observation. A sequence on which it +never stops has bounded sample means that cross each such interval finitely often, so its sample +means converge (Mathlib's `MeasureTheory.tendsto_of_upcrossings_lt_top`). The probability of +stopping under each member of the null is bounded by the upcrossing and maximal inequalities +`ProbabilityTheory.mul_lintegral_upcrossings_sum_div_le` and +`ProbabilityTheory.mul_measure_exists_le_abs_sum_div_sub_le`, which involve the law only through +its centred first absolute moment. The thresholds `K (a, b)` come from summable positive weights +on the rational pairs (`ENNReal.exists_pos_sum_of_countable`). + +## References + +* [RLKR23] J. Ruf, M. Larsson, W. M. Koolen and A. Ramdas, *A composite generalization of Ville's + martingale theorem using e-processes*, Electron. J. Probab. 28 (2023), arXiv:2203.04485v3. +-/ + +public section + +open MeasureTheory Filter TauCeti.Probability +open scoped ENNReal NNReal Topology + +namespace ProbabilityTheory + +/-- The sample mean of the first `n + 1` coordinates is measurable at time `n` for the canonical +filtration. -/ +private lemma measurable_piLE_sum_div (n : ℕ) : + Measurable[Filtration.piLE (X := fun _ : ℕ ↦ ℝ) n] + fun ω : ℕ → ℝ ↦ (∑ i ∈ Finset.range (n + 1), ω i) / (n + 1) := by + refine Measurable.div_const (Finset.measurable_sum _ fun i hi ↦ ?_) _ + exact Filtration.measurable_piLE_apply (Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)) + +/-- A sequence whose sample means stay at distance less than `L` from the first observation and +make fewer than `K q` upcrossings of every interval with rational endpoints `q` has convergent +sample means. -/ +private lemma exists_tendsto_of_upcrossingsBefore_lt {ω : ℕ → ℝ} {L : ℝ} {K : ℚ × ℚ → ℕ} + (hL : ∀ n : ℕ, |(∑ i ∈ Finset.range (n + 1), ω i) / (n + 1) - ω 0| < L) + (hK : ∀ q : ℚ × ℚ, (q.1 : ℝ) < q.2 → ∀ n, upcrossingsBefore q.1 q.2 + (fun n ω ↦ (∑ i ∈ Finset.range (n + 1), ω i) / (n + 1)) n ω < K q) : + ∃ l, Tendsto (fun n : ℕ ↦ (∑ i ∈ Finset.range n, ω i) / n) atTop (𝓝 l) := by + set Y : ℕ → (ℕ → ℝ) → ℝ := fun n ω ↦ (∑ i ∈ Finset.range (n + 1), ω i) / (n + 1) + have hlim : liminf (fun n ↦ (‖Y n ω‖₊ : ℝ≥0∞)) atTop < ⊤ := by + refine (liminf_le_of_frequently_le' (x := ((‖ω 0‖₊ + L.toNNReal : ℝ≥0) : ℝ≥0∞)) + (Eventually.of_forall fun n ↦ ?_).frequently).trans_lt ENNReal.coe_lt_top + rw [ENNReal.coe_le_coe, ← NNReal.coe_le_coe, NNReal.coe_add, coe_nnNorm, coe_nnNorm, + Real.coe_toNNReal', Real.norm_eq_abs, Real.norm_eq_abs] + have h1 := abs_sub_abs_le_abs_sub (Y n ω) (ω 0) + have h2 := hL n + have h3 := le_max_left L 0 + linarith + obtain ⟨l, hl⟩ := tendsto_of_upcrossings_lt_top (f := Y) (ω := ω) hlim fun a b hab ↦ + upcrossings_lt_top_iff.2 ⟨K (a, b), fun N ↦ (hK (a, b) (by exact_mod_cast hab) N).le⟩ + refine ⟨l, (tendsto_add_atTop_iff_nat 1).1 ?_⟩ + simpa [Y] using hl + +/-- The hitting time of a sequence of sets is finite exactly on their union. -/ +private lemma hittingAfter_indicator_lt_top_iff {Ω : Type*} (E : ℕ → Set Ω) (ω : Ω) : + hittingAfter (fun n ↦ (E n).indicator fun _ ↦ (1 : ℝ)) {1} 0 ω < ⊤ ↔ ∃ n, ω ∈ E n := by + rw [lt_top_iff_ne_top, Ne, hittingAfter_eq_top_iff] + push Not + refine exists_congr fun n ↦ ?_ + by_cases h : ω ∈ E n <;> simp [h] + +/-- **A composite strong law of large numbers.** Let `S` be a set of integrable laws on `ℝ` whose +centred first absolute moments `∫ |x - m_P| dP` are at most `c`, where `m_P` is the mean of `P`. +For every `α > 0`, some stopping time of the canonical filtration of `ℕ → ℝ` is finite on every +sequence whose sample means do not converge in `ℝ`, and finite with probability at most `α` under +i.i.d. sampling from each member of `S`. The set of these sequences has thus inverse capital outer +measure zero [RLKR23]. (For a member that is not a probability measure, `Measure.infinitePi` is +zero.) -/ +theorem exists_isStoppingTime_lt_top_of_not_tendsto_mean {S : Set (Measure ℝ)} + (hS : ∀ P ∈ S, Integrable id P) {c : ℝ} (hc : ∀ P ∈ S, ∫ x, |x - ∫ y, y ∂P| ∂P ≤ c) + {α : ℝ≥0∞} (hα : 0 < α) : + ∃ τ : (ℕ → ℝ) → WithTop ℕ, IsStoppingTime (Filtration.piLE (X := fun _ : ℕ ↦ ℝ)) τ ∧ + (∀ P ∈ S, Measure.infinitePi (fun _ : ℕ ↦ P) {ω | τ ω < ⊤} ≤ α) ∧ + ∀ ω : ℕ → ℝ, (¬ ∃ l : ℝ, + Tendsto (fun n : ℕ ↦ (∑ i ∈ Finset.range n, ω i) / n) atTop (𝓝 l)) → τ ω < ⊤ := by + set Y : ℕ → (ℕ → ℝ) → ℝ := fun n ω ↦ (∑ i ∈ Finset.range (n + 1), ω i) / (n + 1) with hY + -- the constants: a level `δ ≤ α`, weights `ε` on the rational pairs, a bound `C` for the + -- centred moments, a distance `L` and the upcrossing thresholds `K` + obtain ⟨δ, hδ0, hδα⟩ := ENNReal.lt_iff_exists_nnreal_btwn.1 hα + have hδ0' : (0 : ℝ≥0) < δ := by exact_mod_cast hδ0 + obtain ⟨ε, hε0, hεsum⟩ := ENNReal.exists_pos_sum_of_countable + (ENNReal.coe_ne_zero.2 (half_pos hδ0').ne') (ℚ × ℚ) + set C : ℝ≥0 := c.toNNReal + 1 with hC + have hcC : c ≤ C := by + rw [hC, NNReal.coe_add, NNReal.coe_one] + linarith [Real.le_coe_toNNReal c] + have hC0 : 0 < C := add_pos_of_nonneg_of_pos zero_le one_pos + set L : ℝ≥0 := 2 * C / δ with hL + set K : ℚ × ℚ → ℕ := fun q ↦ ⌈(C : ℝ) / (((q.2 : ℝ) - q.1) * ε q)⌉₊ + 1 with hK + -- the events at which the stopping time stops + set E : ℕ → Set (ℕ → ℝ) := fun n ↦ {ω | (∃ q : ℚ × ℚ, (q.1 : ℝ) < q.2 ∧ + K q ≤ upcrossingsBefore q.1 q.2 Y n ω) ∨ 2 * (L : ℝ) ≤ |Y n ω - Y 0 ω|} with hE + have hYadapted : StronglyAdapted (Filtration.piLE (X := fun _ : ℕ ↦ ℝ)) Y := + fun n ↦ (measurable_piLE_sum_div n).stronglyMeasurable + have hEmeas (n : ℕ) : MeasurableSet[Filtration.piLE (X := fun _ : ℕ ↦ ℝ) n] (E n) := by + simp only [hE, Set.ofPred_or] + refine MeasurableSet.union ?_ ?_ + · have : {ω | ∃ q : ℚ × ℚ, (q.1 : ℝ) < q.2 ∧ K q ≤ upcrossingsBefore q.1 q.2 Y n ω} = + ⋃ q : ℚ × ℚ, {ω | (q.1 : ℝ) < q.2 ∧ K q ≤ upcrossingsBefore q.1 q.2 Y n ω} := by + ext + simp + rw [this] + refine MeasurableSet.iUnion fun q ↦ ?_ + by_cases hq : (q.1 : ℝ) < q.2 + · simp only [hq, true_and] + exact hYadapted.adapted_upcrossingsBefore hq n (measurableSet_Ici (a := K q)) + · simp [hq] + · refine (continuous_abs.measurable.comp ?_) (measurableSet_Ici (a := 2 * (L : ℝ))) + exact (measurable_piLE_sum_div n).sub + ((measurable_piLE_sum_div 0).mono (Filtration.mono _ (Nat.zero_le n)) le_rfl) + refine ⟨hittingAfter (fun n ↦ (E n).indicator fun _ ↦ (1 : ℝ)) {1} 0, + Adapted.isStoppingTime_hittingAfter (fun n ↦ measurable_const.indicator (hEmeas n)) + (measurableSet_singleton 1), fun P hPS ↦ ?_, fun ω hω ↦ ?_⟩ + · by_cases hP₁ : IsProbabilityMeasure P + swap + · -- the product of copies of `P` is zero + have : Measure.infinitePi (fun _ : ℕ ↦ P) = 0 := by + simp only [Measure.infinitePi] + exact dite_eq_right fun h ↦ hP₁ (h 0) + simp [this] + set μ := Measure.infinitePi fun _ : ℕ ↦ P + set m := ∫ y, y ∂P + -- the i.i.d. law is exchangeable, and its first coordinate is integrable of law `P` + have hμ : ExchangeableLaw μ := exchangeableLaw_infinitePi_const ⟨P, hP₁⟩ + have hint : Integrable (fun ω ↦ ω 0) μ := + ((measurePreserving_eval_infinitePi (fun _ : ℕ ↦ P) 0).integrable_comp + (hS P hPS).aestronglyMeasurable).2 (hS P hPS) + have hm : ∫ ω, ω 0 ∂μ = m := integral_comp_eval_infinitePi (μ := fun _ : ℕ ↦ P) (i := 0) + (f := fun x ↦ x) aestronglyMeasurable_id + have hc₀ : ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ) ≤ C := by + have h : ∫ ω, |ω 0 - m| ∂μ = ∫ x, |x - m| ∂P := + integral_comp_eval_infinitePi (μ := fun _ : ℕ ↦ P) (i := 0) (f := fun x ↦ |x - m|) + (by fun_prop) + refine ENNReal.ofReal_le_of_le_toReal ?_ + rw [ENNReal.coe_toReal, h] + exact (hc P hPS).trans hcC + -- stopping means many upcrossings of some interval, or a sample mean far from `m` + have hsub : {ω | hittingAfter (fun n ↦ (E n).indicator fun _ ↦ (1 : ℝ)) {1} 0 ω < ⊤} ⊆ + (⋃ q : ℚ × ℚ, {ω | (q.1 : ℝ) < q.2 ∧ (K q : ℝ≥0∞) ≤ upcrossings q.1 q.2 Y ω}) ∪ + {ω | ∃ n, (L : ℝ) ≤ |Y n ω - m|} := by + intro ω hω + rw [Set.mem_ofPred_eq, hittingAfter_indicator_lt_top_iff] at hω + obtain ⟨n, hn⟩ := hω + rcases hn with ⟨q, hq, hKq⟩ | hfar + · refine Or.inl (Set.mem_iUnion.2 ⟨q, hq, ?_⟩) + exact (Nat.cast_le.2 hKq).trans + (le_iSup (fun N ↦ (upcrossingsBefore q.1 q.2 Y N ω : ℝ≥0∞)) n) + · refine Or.inr ?_ + by_contra h + simp only [Set.mem_ofPred_eq, not_exists, not_le] at h + have h1 := h n + have h0 := h 0 + have := abs_sub_le (Y n ω) m (Y 0 ω) + rw [abs_sub_comm m] at this + linarith + -- many upcrossings of `[q.1, q.2]` have probability at most `ε q` + have hq (q : ℚ × ℚ) : + μ {ω | (q.1 : ℝ) < q.2 ∧ (K q : ℝ≥0∞) ≤ upcrossings q.1 q.2 Y ω} ≤ ε q := by + by_cases hq : (q.1 : ℝ) < q.2 + swap + · simp [hq] + simp only [hq, true_and] + set x := ENNReal.ofReal ((q.2 : ℝ) - q.1) * K q + have hx0 : x ≠ 0 := mul_ne_zero (ENNReal.ofReal_pos.2 (sub_pos.2 hq)).ne' (by simp [hK]) + have hxtop : x ≠ ⊤ := ENNReal.mul_ne_top ENNReal.ofReal_ne_top (ENNReal.natCast_ne_top _) + have hreal : (C : ℝ) ≤ ((q.2 : ℝ) - q.1) * K q * ε q := by + have hd : 0 < ((q.2 : ℝ) - q.1) * ε q := mul_pos (sub_pos.2 hq) (hε0 q) + have hceil := Nat.le_ceil ((C : ℝ) / (((q.2 : ℝ) - q.1) * ε q)) + have hKq : (C : ℝ) / (((q.2 : ℝ) - q.1) * ε q) ≤ K q := by + simp only [hK, Nat.cast_add, Nat.cast_one] + linarith + calc (C : ℝ) ≤ K q * (((q.2 : ℝ) - q.1) * ε q) := (div_le_iff₀ hd).1 hKq + _ = ((q.2 : ℝ) - q.1) * K q * ε q := by ring + rw [← ENNReal.mul_le_mul_iff_right hx0 hxtop] + calc x * μ {ω | (K q : ℝ≥0∞) ≤ upcrossings q.1 q.2 Y ω} + = ENNReal.ofReal ((q.2 : ℝ) - q.1) * + (K q * μ {ω | (K q : ℝ≥0∞) ≤ upcrossings q.1 q.2 Y ω}) := mul_assoc _ _ _ + _ ≤ ENNReal.ofReal ((q.2 : ℝ) - q.1) * ∫⁻ ω, upcrossings q.1 q.2 Y ω ∂μ := by + gcongr + exact mul_meas_ge_le_lintegral₀ + (hYadapted.measurable_upcrossings hq).aemeasurable _ + _ ≤ ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ) := by + simpa only [hm] using mul_lintegral_upcrossings_sum_div_le hμ hint q.1 q.2 + _ ≤ C := hc₀ + _ = ENNReal.ofReal C := ENNReal.ofReal_coe_nnreal.symm + _ ≤ ENNReal.ofReal (((q.2 : ℝ) - q.1) * K q * ε q) := ENNReal.ofReal_le_ofReal hreal + _ = x * ε q := by + rw [ENNReal.ofReal_mul (mul_nonneg (sub_nonneg.2 hq.le) (Nat.cast_nonneg _)), + ENNReal.ofReal_mul (sub_nonneg.2 hq.le), ENNReal.ofReal_natCast, + ENNReal.ofReal_coe_nnreal] + -- a sample mean at distance at least `L` from `m` has probability at most `δ / 2` + have hfar : μ {ω | ∃ n, (L : ℝ) ≤ |Y n ω - m|} ≤ ((δ / 2 : ℝ≥0) : ℝ≥0∞) := by + have hL0 : (L : ℝ≥0∞) ≠ 0 := by + rw [ENNReal.coe_ne_zero, hL] + positivity + rw [← ENNReal.mul_le_mul_iff_right hL0 ENNReal.coe_ne_top] + refine (mul_measure_exists_le_abs_sum_div_sub_le hμ hint m L).trans (hc₀.trans_eq ?_) + rw [← ENNReal.coe_mul, show L * (δ / 2) = C by rw [hL]; field_simp] + calc μ {ω | hittingAfter (fun n ↦ (E n).indicator fun _ ↦ (1 : ℝ)) {1} 0 ω < ⊤} + ≤ ∑' q : ℚ × ℚ, μ {ω | (q.1 : ℝ) < q.2 ∧ (K q : ℝ≥0∞) ≤ upcrossings q.1 q.2 Y ω} + + μ {ω | ∃ n, (L : ℝ) ≤ |Y n ω - m|} := + (measure_mono hsub).trans ((measure_union_le _ _).trans + (add_le_add_left (measure_iUnion_le _) _)) + _ ≤ ∑' q, (ε q : ℝ≥0∞) + ((δ / 2 : ℝ≥0) : ℝ≥0∞) := add_le_add (tsum_le_tsum hq) hfar + _ ≤ ((δ / 2 : ℝ≥0) : ℝ≥0∞) + ((δ / 2 : ℝ≥0) : ℝ≥0∞) := by gcongr + _ = δ := by rw [← ENNReal.coe_add, add_halves] + _ ≤ α := hδα.le + · -- a sequence on which the stopping time is infinite has convergent sample means + rw [hittingAfter_indicator_lt_top_iff] + by_contra h + simp only [hE, Set.mem_ofPred_eq, not_exists, not_or, not_and, not_le] at h + refine hω (exists_tendsto_of_upcrossingsBefore_lt (L := 2 * L) (K := K) (fun n ↦ ?_) + fun q hq n ↦ (h n).1 q hq) + simpa [Y] using (h n).2 + +end ProbabilityTheory diff --git a/LMLExplore/Probability/Martingale/SampleMean.lean b/LMLExplore/Probability/Martingale/SampleMean.lean new file mode 100644 index 00000000..96b89076 --- /dev/null +++ b/LMLExplore/Probability/Martingale/SampleMean.lean @@ -0,0 +1,285 @@ +/- +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.Probability.Martingale.Upcrossing +public import TauCeti.Probability.Exchangeability.PathSpace.Law.Basic +import LMLExplore.Probability.Martingale.Upcrossing +import Mathlib.MeasureTheory.MeasurableSpace.Invariants +import TauCeti.Probability.Martingale.Crossings.Pathwise +import TauCeti.Probability.Martingale.MaximalInequality.Basic +import TauCeti.Probability.Martingale.Reverse + +/-! +# Maximal and upcrossing inequalities for the sample means of an exchangeable sequence + +Let `μ` be an exchangeable law of a sequence `X₀, X₁, …` of real random variables (a probability +measure on `ℕ → ℝ` invariant under the permutations of the coordinates, Tau Ceti's +`TauCeti.Probability.ExchangeableLaw`), for instance the law `Measure.infinitePi fun _ ↦ P` of an +i.i.d. sequence, with `X₀` integrable of mean `m`. Let `X̄ₙ = (X₀ + ⋯ + Xₙ) / (n + 1)`. For a +horizon `N`, the sample means read backwards, `k ↦ X̄_{N - k}`, form a martingale for the +σ-algebras of the events that are symmetric in the first `N - k + 1` coordinates. Doob's +inequalities for this martingale give two bounds that hold uniformly in the horizon: + +* for every `m' : ℝ`, the sample means come at distance at least `L` from `m'` with probability + at most `𝔼|X₀ - m'| / L`; +* the expected number of upcrossings of `[a, b]` by the sample means is at most + `𝔼|X₀ - m| / (b - a)`. + +The second bound does not depend on the position of `[a, b]` relative to `m`. It rests on Doob's +upcrossing inequality with the initial term, +`MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_posPart_sub`, which bounds +the expected upcrossings of `[-b, -a]` by the negated reversed means by +`𝔼(b - X₀)⁺ - (b - m)⁺ ≤ 𝔼|X₀ - m|`, and on Tau Ceti's comparison of the upcrossings of a process +with those of its negated time reversal. + +## Main statements + +* `ProbabilityTheory.mul_measure_exists_le_abs_sum_div_sub_le`: the maximal inequality. +* `ProbabilityTheory.mul_lintegral_upcrossings_sum_div_le`: the upcrossing inequality. +-/ + +public section + +open MeasureTheory TauCeti.Probability +open scoped ENNReal NNReal + +namespace ProbabilityTheory + +variable {μ : Measure (ℕ → ℝ)} + +/-! ### Swaps of coordinates and symmetric events -/ + +/-- The swap of the coordinates `0` and `i` of a sequence. -/ +private abbrev swapAt (i : ℕ) : (ℕ → ℝ) → ℕ → ℝ := permReindex (Equiv.swap 0 i) + +/-- Swapping the coordinates `0` and `i` twice gives back the sequence. -/ +private lemma swapAt_involutive (i : ℕ) : Function.Involutive (swapAt i) := fun ω ↦ by + ext j + simp + +/-- On a set invariant under the swap of the coordinates `0` and `i`, the coordinates `0` and `i` +of an exchangeable sequence have the same integral. -/ +private lemma setIntegral_apply_eq_of_preimage_swapAt_eq (hμ : ExchangeableLaw μ) {i : ℕ} + {s : Set (ℕ → ℝ)} (hs : swapAt i ⁻¹' s = s) : + ∫ ω in s, ω i ∂μ = ∫ ω in s, ω 0 ∂μ := by + have h := (hμ.measurePreserving_permReindex (Equiv.swap 0 i)).setIntegral_preimage_emb + (MeasurableEquiv.ofInvolutive _ (swapAt_involutive i) + (measurable_reindex _)).measurableEmbedding (fun ω ↦ ω 0) s + rw [hs] at h + simpa using h + +/-- The coordinates of an exchangeable sequence whose first coordinate is integrable are +integrable. -/ +private lemma integrable_apply (hμ : ExchangeableLaw μ) (hint : Integrable (fun ω ↦ ω 0) μ) + (i : ℕ) : Integrable (fun ω : ℕ → ℝ ↦ ω i) μ := by + simpa [Function.comp_def] using + ((hμ.measurePreserving_permReindex (Equiv.swap 0 i)).integrable_comp + hint.aestronglyMeasurable).2 hint + +/-- The σ-algebra of the measurable events that are invariant under the swap of the coordinates +`0` and `i` for every `i ≤ n`, that is, symmetric in the first `n + 1` coordinates. -/ +@[instance_reducible] +private def symmLE (n : ℕ) : MeasurableSpace (ℕ → ℝ) := + ⨅ i ≤ n, MeasurableSpace.invariants (swapAt i) + +/-- An event is symmetric in the first `n + 1` coordinates when it is measurable and invariant +under the swaps of the coordinates `0` and `i ≤ n`. -/ +private lemma measurableSet_symmLE_iff {n : ℕ} {s : Set (ℕ → ℝ)} : + MeasurableSet[symmLE n] s ↔ ∀ i ≤ n, MeasurableSet s ∧ swapAt i ⁻¹' s = s := by + simp only [MeasurableSpace.measurableSet_iInf, MeasurableSpace.measurableSet_invariants] + +/-- Fewer events are symmetric in more coordinates. -/ +private lemma symmLE_anti : Antitone symmLE := fun _ _ hnm ↦ + biInf_mono fun _ hi ↦ hi.trans hnm + +/-- The symmetric events are measurable. -/ +private lemma symmLE_le (n : ℕ) : symmLE n ≤ MeasurableSpace.pi := + (iInf₂_le 0 (Nat.zero_le n)).trans (MeasurableSpace.invariants_le _) + +/-! ### The reverse martingale of the sample means -/ + +/-- The mean of the coordinates `0, …, n` of a sequence. -/ +private noncomputable def smean (n : ℕ) (ω : ℕ → ℝ) : ℝ := + (∑ i ∈ Finset.range (n + 1), ω i) / (n + 1) + +/-- The mean of the coordinate `0` alone is that coordinate. -/ +private lemma smean_zero (ω : ℕ → ℝ) : smean 0 ω = ω 0 := by simp [smean] + +/-- The sample means are measurable. -/ +private lemma measurable_smean (n : ℕ) : Measurable (smean n) := by + unfold smean + fun_prop + +/-- The mean of the coordinates `0, …, n` is invariant under the swap of the coordinates `0` and +`i ≤ n`. -/ +private lemma smean_swapAt {n i : ℕ} (hi : i ≤ n) (ω : ℕ → ℝ) : + smean n (swapAt i ω) = smean n ω := by + simp only [smean, swapAt, permReindex_apply] + congr 1 + refine Equiv.Perm.sum_comp (Equiv.swap 0 i) (Finset.range (n + 1)) ω fun j hj ↦ ?_ + simp only [Set.mem_ofPred_eq] at hj + simp only [Finset.coe_range, Set.mem_Iio] + by_contra! h + exact hj (Equiv.swap_apply_of_ne_of_ne (by omega) (by omega)) + +/-- The mean of the coordinates `0, …, n` is measurable for the events symmetric in them. -/ +private lemma measurable_symmLE_smean (n : ℕ) : Measurable[symmLE n] (smean n) := by + intro t ht + rw [measurableSet_symmLE_iff] + intro i hi + refine ⟨measurable_smean n ht, ?_⟩ + ext ω + simp only [Set.mem_preimage, smean_swapAt hi] + +/-- The sample means of an exchangeable sequence with an integrable first coordinate are +integrable. -/ +private lemma integrable_smean (hμ : ExchangeableLaw μ) (hint : Integrable (fun ω ↦ ω 0) μ) + (n : ℕ) : Integrable (smean n) μ := + (integrable_finsetSum _ fun i _ ↦ integrable_apply hμ hint i).div_const _ + +/-- On an event symmetric in the first `n + 1` coordinates, the integral of the mean of the +coordinates `0, …, m`, for `m ≤ n`, is that of the coordinate `0`. -/ +private lemma setIntegral_smean_eq (hμ : ExchangeableLaw μ) (hint : Integrable (fun ω ↦ ω 0) μ) + {n m : ℕ} (hmn : m ≤ n) {s : Set (ℕ → ℝ)} (hs : MeasurableSet[symmLE n] s) : + ∫ ω in s, smean m ω ∂μ = ∫ ω in s, ω 0 ∂μ := by + rw [measurableSet_symmLE_iff] at hs + unfold smean + rw [integral_div, integral_finsetSum _ fun i _ ↦ (integrable_apply hμ hint i).integrableOn, + Finset.sum_congr rfl fun i hi ↦ setIntegral_apply_eq_of_preimage_swapAt_eq hμ + (hs i ((Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)).trans hmn)).2, + Finset.sum_const, Finset.card_range, nsmul_eq_mul] + push_cast + field_simp + +/-- The integral of a sample mean is that of the first coordinate. -/ +private lemma integral_smean (hμ : ExchangeableLaw μ) (hint : Integrable (fun ω ↦ ω 0) μ) + (n : ℕ) : ∫ ω, smean n ω ∂μ = ∫ ω, ω 0 ∂μ := by + simpa using setIntegral_smean_eq hμ hint le_rfl (MeasurableSet.univ (m := symmLE n)) + +/-- Under an exchangeable law with an integrable first coordinate, the sample means read backwards +from the horizon `N` form a martingale. -/ +private lemma martingale_smean_rev [IsFiniteMeasure μ] (hμ : ExchangeableLaw μ) + (hint : Integrable (fun ω ↦ ω 0) μ) (N : ℕ) : + Martingale (fun k ↦ smean (N - k)) (revFiltration symmLE symmLE_anti symmLE_le N) μ := by + refine martingale_of_setIntegral_eq_succ (fun k ↦ ?_) (fun k ↦ integrable_smean hμ hint _) + fun k s hs ↦ ?_ + · rw [revFiltration_apply] + exact (measurable_symmLE_smean (N - k)).stronglyMeasurable + · rw [revFiltration_apply] at hs + rw [setIntegral_smean_eq hμ hint le_rfl hs, setIntegral_smean_eq hμ hint (by omega) hs] + +/-! ### The maximal inequality -/ + +/-- **Maximal inequality for the sample means of an exchangeable sequence**: if the first +coordinate is integrable, then for every `m : ℝ` the probability that some sample mean is at +distance at least `L` from `m` is at most `∫ |X₀ - m| / L`. -/ +theorem mul_measure_exists_le_abs_sum_div_sub_le [IsFiniteMeasure μ] (hμ : ExchangeableLaw μ) + (hint : Integrable (fun ω ↦ ω 0) μ) (m : ℝ) (L : ℝ≥0) : + L * μ {ω | ∃ n : ℕ, (L : ℝ) ≤ |(∑ i ∈ Finset.range (n + 1), ω i) / (n + 1) - m|} ≤ + ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ) := by + change L * μ {ω | ∃ n : ℕ, (L : ℝ) ≤ |smean n ω - m|} ≤ _ + -- the event is the increasing union of the events up to the horizons `N` + have hset : {ω | ∃ n : ℕ, (L : ℝ) ≤ |smean n ω - m|} = + ⋃ N, {ω | ∃ n ≤ N, (L : ℝ) ≤ |smean n ω - m|} := by + ext ω + simp only [Set.mem_ofPred_eq, Set.mem_iUnion] + exact ⟨fun ⟨n, hn⟩ ↦ ⟨n, n, le_rfl, hn⟩, fun ⟨_, n, _, hn⟩ ↦ ⟨n, hn⟩⟩ + have hmono : Monotone fun N ↦ {ω | ∃ n ≤ N, (L : ℝ) ≤ |smean n ω - m|} := + fun _ _ h _ ⟨n, hn, hn'⟩ ↦ ⟨n, hn.trans h, hn'⟩ + rw [hset, hmono.measure_iUnion, ENNReal.mul_iSup] + refine iSup_le fun N ↦ ?_ + -- Doob's maximal inequality for the submartingale `k ↦ |X̄_{N - k} - m|` + have hM := ((martingale_smean_rev hμ hint N).sub (martingale_const _ _ m)).submartingale_norm + have h : L * μ {ω | ∃ k ∈ Finset.range (N + 1), (L : ℝ) ≤ |smean (N - k) ω - m|} ≤ + ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ) := by + simpa [Real.norm_eq_abs, smean_zero] using hM.mul_measure_exists_mem_le_le + (fun _ _ ↦ norm_nonneg _) L (F := Finset.range (N + 1)) (T := N) + fun _ ht ↦ Nat.lt_succ_iff.1 (Finset.mem_range.1 ht) + refine le_trans (mul_le_mul' le_rfl (measure_mono ?_)) h + rintro ω ⟨n, hn, hL⟩ + exact ⟨N - n, Finset.mem_range.2 (by omega), by rwa [Nat.sub_sub_self hn]⟩ + +/-! ### The upcrossing inequality -/ + +/-- The upcrossings of `[a, b]` by the sample means before `N` are upcrossings of `[-b, -a]` by +the negated sample means read backwards from the horizon `N`, before `N + 1`. -/ +private lemma upcrossingsBefore_smean_le {a b : ℝ} (hab : a < b) (N : ℕ) (ω : ℕ → ℝ) : + upcrossingsBefore a b smean N ω ≤ + upcrossingsBefore (-b) (-a) (-fun k ↦ smean (N - k)) (N + 1) ω := by + refine (upcrossingsBefore_le_upcrossingsBefore_neg_revProcess_succ smean a b hab N ω).trans_eq ?_ + refine upcrossingsBefore_succ_congr fun k hk ↦ ?_ + simp only [Pi.neg_apply, revProcess_apply_of_le _ hk] + +/-- **Upcrossing inequality for the sample means of an exchangeable sequence**: if the first +coordinate `X₀` is integrable, of mean `m`, the expected number of upcrossings of `[a, b]` by the +sample means is at most `∫ |X₀ - m| / (b - a)`. -/ +theorem mul_lintegral_upcrossings_sum_div_le [IsProbabilityMeasure μ] (hμ : ExchangeableLaw μ) + (hint : Integrable (fun ω ↦ ω 0) μ) (a b : ℝ) : + ENNReal.ofReal (b - a) * + ∫⁻ ω, upcrossings a b (fun n ω ↦ (∑ i ∈ Finset.range (n + 1), ω i) / (n + 1)) ω ∂μ ≤ + ENNReal.ofReal (∫ ω, |ω 0 - ∫ ω', ω' 0 ∂μ| ∂μ) := by + rcases le_or_gt b a with hba | hab + · simp [ENNReal.ofReal_of_nonpos (sub_nonpos.2 hba)] + set m := ∫ ω, ω 0 ∂μ + change ENNReal.ofReal (b - a) * ∫⁻ ω, upcrossings a b smean ω ∂μ ≤ _ + -- monotone convergence in the horizon + have hadapted : StronglyAdapted (Filtration.const ℕ MeasurableSpace.pi le_rfl) smean := + fun n ↦ (measurable_smean n).stronglyMeasurable + simp only [upcrossings] + rw [lintegral_iSup (f := fun N ω ↦ (upcrossingsBefore a b smean N ω : ℝ≥0∞)) + (fun N ↦ measurable_from_top.comp (hadapted.measurable_upcrossingsBefore hab)) + (fun _ _ h ω ↦ Nat.cast_le.2 (upcrossingsBefore_mono hab h ω)), ENNReal.mul_iSup] + refine iSup_le fun N ↦ ?_ + -- Doob's upcrossing inequality for the negated reversed means + have hM := (martingale_smean_rev hμ hint N).neg + have hint' := hM.stronglyAdapted.integrable_upcrossingsBefore (μ := μ) (N := N + 1) + (neg_lt_neg hab) + have hDoob := hM.submartingale.mul_integral_upcrossingsBefore_le_integral_posPart_sub + (-b) (-a) (N + 1) + rw [neg_sub_neg] at hDoob + simp only [Pi.neg_apply, Nat.sub_eq_zero_of_le (Nat.le_succ N), Nat.sub_zero, smean_zero, + sub_neg_eq_add, neg_add_eq_sub] at hDoob + -- the expectation at time `0` is at least `(b - m)⁺`, by convexity + have hb : Integrable (fun ω ↦ b - smean N ω) μ := (integrable_const b).sub + (integrable_smean hμ hint N) + have h₁ : (b - m)⁺ ≤ ∫ ω, (b - smean N ω)⁺ ∂μ := by + have heq : ∫ ω, (b - smean N ω) ∂μ = b - m := by + rw [integral_sub (integrable_const b) (integrable_smean hμ hint N), integral_const, + probReal_univ, one_smul, integral_smean hμ hint N] + rw [← heq, posPart_def] + exact sup_le (integral_mono hb hb.pos_part fun ω ↦ le_posPart _) + (integral_nonneg fun ω ↦ posPart_nonneg _) + -- `(b - x)⁺ - (b - m)⁺ ≤ |x - m|`, the positive part being `1`-Lipschitz + have h₂ : ∫ ω, (b - ω 0)⁺ ∂μ - (b - m)⁺ ≤ ∫ ω, |ω 0 - m| ∂μ := by + have key (x : ℝ) : (b - x)⁺ - (b - m)⁺ ≤ |x - m| := by + rw [sub_le_iff_le_add, posPart_def, posPart_def] + refine sup_le ?_ ?_ + · have := le_sup_left (a := b - m) (b := 0) + have := neg_abs_le (x - m) + linarith + · have := le_sup_right (a := b - m) (b := 0) + have := abs_nonneg (x - m) + linarith + have hint₀ : Integrable (fun ω ↦ (b - ω 0)⁺) μ := ((integrable_const b).sub hint).pos_part + calc ∫ ω, (b - ω 0)⁺ ∂μ - (b - m)⁺ = ∫ ω, ((b - ω 0)⁺ - (b - m)⁺) ∂μ := by + rw [integral_sub hint₀ (integrable_const _), integral_const, probReal_univ, one_smul] + _ ≤ ∫ ω, |ω 0 - m| ∂μ := integral_mono (hint₀.sub (integrable_const _)) + (hint.sub (integrable_const m)).abs fun ω ↦ key (ω 0) + calc ENNReal.ofReal (b - a) * ∫⁻ ω, (upcrossingsBefore a b smean N ω : ℝ≥0∞) ∂μ + ≤ ENNReal.ofReal (b - a) * ∫⁻ ω, + (upcrossingsBefore (-b) (-a) (-fun k ↦ smean (N - k)) (N + 1) ω : ℝ≥0∞) ∂μ := by + gcongr with ω + exact_mod_cast upcrossingsBefore_smean_le hab N ω + _ = ENNReal.ofReal ((b - a) * ∫ ω, + (upcrossingsBefore (-b) (-a) (-fun k ↦ smean (N - k)) (N + 1) ω : ℝ) ∂μ) := by + rw [ENNReal.ofReal_mul (sub_nonneg.2 hab.le), + ofReal_integral_eq_lintegral_ofReal hint' (.of_forall fun ω ↦ Nat.cast_nonneg _)] + simp + _ ≤ ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ) := + ENNReal.ofReal_le_ofReal (by linarith) + +end ProbabilityTheory diff --git a/LMLExplore/Probability/Martingale/Upcrossing.lean b/LMLExplore/Probability/Martingale/Upcrossing.lean new file mode 100644 index 00000000..fb779f4d --- /dev/null +++ b/LMLExplore/Probability/Martingale/Upcrossing.lean @@ -0,0 +1,85 @@ +/- +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.Probability.Martingale.Upcrossing + +/-! +# Doob's upcrossing inequality with the initial term + +For a real submartingale `f`, a time `N` and real numbers `a`, `b`, the number `U_N` of upcrossings +of `[a, b]` that `f` completes before `N` satisfies Doob's inequality + +`(b - a) 𝔼[U_N] ≤ 𝔼[(f N - a)⁺] - 𝔼[(f 0 - a)⁺]`. + +Mathlib's `MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part` drops +the last term. Keeping it matters when the bound must not depend on the location of the process: +for a martingale started at a value of mean `m`, the right-hand side is at most +`𝔼[(f N - a)⁺] - (m - a)⁺`, which stays bounded as `a` and `b` move away from `m`. + +The number of upcrossings completed before `N` is a function of the process up to time `N`, so +the upcrossing counts of an adapted process form an adapted process. + +## Main statements + +* `MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_posPart_sub`: Doob's + upcrossing inequality with the initial term. +* `MeasureTheory.StronglyAdapted.adapted_upcrossingsBefore`: the upcrossing counts of an adapted + process are adapted. +-/ + +public section + +namespace MeasureTheory + +variable {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ℕ m0} + {f : ℕ → Ω → ℝ} {a b : ℝ} + +/-- The number of upcrossings of `[a, b]` that an adapted process completes before time `N` is +measurable at time `N`: the upcrossing counts form an adapted process. -/ +theorem StronglyAdapted.adapted_upcrossingsBefore (hf : StronglyAdapted ℱ f) (hab : a < b) : + Adapted ℱ fun N ↦ upcrossingsBefore a b f N := by + intro N + dsimp only + have : upcrossingsBefore a b f N = fun ω ↦ + ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i := by + ext ω + exact upcrossingsBefore_eq_sum hab + rw [this] + refine Finset.measurable_fun_sum _ fun i _ ↦ Measurable.indicator + (s := {ω | upperCrossingTime a b f N i ω < N}) measurable_const ?_ + simpa only [ENat.some_eq_natCast, Nat.cast_lt] using! + hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N + +/-- **Doob's upcrossing inequality** with the initial term: for a submartingale `f`, +`(b - a) 𝔼[U_N] ≤ 𝔼[(f N - a)⁺] - 𝔼[(f 0 - a)⁺]`, where `U_N` is the number of upcrossings of +`[a, b]` completed before `N`. -/ +theorem Submartingale.mul_integral_upcrossingsBefore_le_integral_posPart_sub [IsFiniteMeasure μ] + (a b : ℝ) (hf : Submartingale f ℱ μ) (N : ℕ) : + (b - a) * ∫ ω, (upcrossingsBefore a b f N ω : ℝ) ∂μ ≤ + ∫ ω, (f N ω - a)⁺ ∂μ - ∫ ω, (f 0 ω - a)⁺ ∂μ := by + set g : ℕ → Ω → ℝ := fun n ω ↦ (f n ω - a)⁺ with hg_def + have hg : Submartingale g ℱ μ := (hf.sub_martingale (martingale_const _ _ a)).pos + rcases le_or_gt b a with hba | hab + · -- the left-hand side is nonpositive and the right-hand side is nonnegative + refine (mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.2 hba) + (integral_nonneg fun ω ↦ Nat.cast_nonneg _)).trans ?_ + exact sub_nonneg.2 (by simpa using hg.setIntegral_le (Nat.zero_le N) MeasurableSet.univ) + have hab' : (0 : ℝ) < b - a := sub_pos.2 hab + calc (b - a) * ∫ ω, (upcrossingsBefore a b f N ω : ℝ) ∂μ + = (b - a) * ∫ ω, (upcrossingsBefore 0 (b - a) g N ω : ℝ) ∂μ := by + simp_rw [hg_def, upcrossingsBefore_pos_eq hab] + _ ≤ ∫ ω, (∑ k ∈ Finset.range N, + upcrossingStrat 0 (b - a) g N k * (g (k + 1) - g k)) ω ∂μ := by + rw [← integral_const_mul] + refine integral_mono_of_nonneg ?_ + ((hg.sum_upcrossingStrat_mul 0 (b - a) N).integrable N) ?_ + · exact .of_forall fun ω ↦ mul_nonneg hab'.le (Nat.cast_nonneg _) + · filter_upwards with ω + simpa [sub_zero] using mul_upcrossingsBefore_le (f := g) (posPart_nonneg _) hab' + _ ≤ ∫ ω, g N ω ∂μ - ∫ ω, g 0 ω ∂μ := hg.sum_mul_upcrossingStrat_le + +end MeasureTheory From fde588be6a1ca1ffe396da9bd95d82c2e4e9fee5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:56:43 +0100 Subject: [PATCH 2/2] style: replace the combining macron in sample-mean notation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The unicode style linter rejects U+0304 (combining macron) in `X̄ₙ`; write the sample means as `Aₙ` instead. Co-Authored-By: Claude Code --- LMLExplore/EValues/CompositeStrongLaw.lean | 7 ++++--- LMLExplore/Probability/Martingale/SampleMean.lean | 6 +++--- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/LMLExplore/EValues/CompositeStrongLaw.lean b/LMLExplore/EValues/CompositeStrongLaw.lean index 6adbce82..b16f0cf5 100644 --- a/LMLExplore/EValues/CompositeStrongLaw.lean +++ b/LMLExplore/EValues/CompositeStrongLaw.lean @@ -38,9 +38,10 @@ strong law implies this hypothesis. ## Implementation notes -The stopping time stops at the first time `n` at which, for some interval `[a, b]` with rational -endpoints, the sample means `X̄₁, …, X̄ₙ₊₁` have completed `K (a, b)` upcrossings of `[a, b]`, or -at which `X̄ₙ₊₁` is at distance at least `2 L` from the first observation. A sequence on which it +Write `Aₖ` for the mean of the first `k` observations. The stopping time stops at the first time +`n` at which, for some interval `[a, b]` with rational endpoints, the sample means +`A₁, …, Aₙ₊₁` have completed `K (a, b)` upcrossings of `[a, b]`, or +at which `Aₙ₊₁` is at distance at least `2 L` from the first observation. A sequence on which it never stops has bounded sample means that cross each such interval finitely often, so its sample means converge (Mathlib's `MeasureTheory.tendsto_of_upcrossings_lt_top`). The probability of stopping under each member of the null is bounded by the upcrossing and maximal inequalities diff --git a/LMLExplore/Probability/Martingale/SampleMean.lean b/LMLExplore/Probability/Martingale/SampleMean.lean index 96b89076..739a902b 100644 --- a/LMLExplore/Probability/Martingale/SampleMean.lean +++ b/LMLExplore/Probability/Martingale/SampleMean.lean @@ -19,8 +19,8 @@ import TauCeti.Probability.Martingale.Reverse Let `μ` be an exchangeable law of a sequence `X₀, X₁, …` of real random variables (a probability measure on `ℕ → ℝ` invariant under the permutations of the coordinates, Tau Ceti's `TauCeti.Probability.ExchangeableLaw`), for instance the law `Measure.infinitePi fun _ ↦ P` of an -i.i.d. sequence, with `X₀` integrable of mean `m`. Let `X̄ₙ = (X₀ + ⋯ + Xₙ) / (n + 1)`. For a -horizon `N`, the sample means read backwards, `k ↦ X̄_{N - k}`, form a martingale for the +i.i.d. sequence, with `X₀` integrable of mean `m`. Let `Aₙ = (X₀ + ⋯ + Xₙ) / (n + 1)`. For a +horizon `N`, the sample means read backwards, `k ↦ A_{N - k}`, form a martingale for the σ-algebras of the events that are symmetric in the first `N - k + 1` coordinates. Doob's inequalities for this martingale give two bounds that hold uniformly in the horizon: @@ -192,7 +192,7 @@ theorem mul_measure_exists_le_abs_sum_div_sub_le [IsFiniteMeasure μ] (hμ : Exc fun _ _ h _ ⟨n, hn, hn'⟩ ↦ ⟨n, hn.trans h, hn'⟩ rw [hset, hmono.measure_iUnion, ENNReal.mul_iSup] refine iSup_le fun N ↦ ?_ - -- Doob's maximal inequality for the submartingale `k ↦ |X̄_{N - k} - m|` + -- Doob's maximal inequality for the submartingale `k ↦ |A_{N - k} - m|` have hM := ((martingale_smean_rev hμ hint N).sub (martingale_const _ _ m)).submartingale_norm have h : L * μ {ω | ∃ k ∈ Finset.range (N + 1), (L : ℝ) ≤ |smean (N - k) ω - m|} ≤ ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ) := by