From 21c8cc2e42f09cfb3286e88bb9be1fe476ecc95b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 16:09:04 +0100 Subject: [PATCH 1/2] feat: e-processes for an i.i.d. null grow at most at the bipolar rate, almost surely Prove that, for every sequence of n-sample e-variables for an i.i.d. null, almost surely under the i.i.d. law of the alternative, the n-th one evaluated at the first n observations has limsup (1/n) log at most the bipolar rate; also for functions of the first n observations with expectation at most one under the null, and for e-processes per observation seen. This is the almost sure upper bound of EValues, Layer 6, item 1. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- .../EValues/BipolarRate/AlmostSure.lean | 831 ++++++++++++++++++ 1 file changed, 831 insertions(+) create mode 100644 LMLExplore/EValues/BipolarRate/AlmostSure.lean diff --git a/LMLExplore/EValues/BipolarRate/AlmostSure.lean b/LMLExplore/EValues/BipolarRate/AlmostSure.lean new file mode 100644 index 00000000..1caebead --- /dev/null +++ b/LMLExplore/EValues/BipolarRate/AlmostSure.lean @@ -0,0 +1,831 @@ +/- +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.EValues.BipolarRate.EProcess +import Mathlib.Probability.Independence.Integration +import TauCeti.Probability.Ergodic.BernoulliShift + +/-! +# E-processes for an i.i.d. null grow at most at the bipolar rate, almost surely + +Let `S₁` be a set of probability measures on `𝓧` (the null) and `Q₁` a law on `𝓧` (the +alternative). The observations are the coordinates of `ℕ → 𝓧`, with the i.i.d. laws +`Measure.infinitePi fun _ ↦ P`. For every sequence of `n`-sample e-variables `M n` for the +i.i.d. null, almost surely under the i.i.d. law of `Q₁`, `M n` evaluated at the first `n` +observations has `limsup (1/n) log (M n) ≤ bipolarRate Q₁ S₁`. In particular an e-process for the +i.i.d. null grows almost surely at most at the bipolar rate per observation. The members of `S₁` +are probability measures, and nothing else is assumed on `S₁` or `Q₁`: no domination, convexity +or compactness. Since the bipolar rate is at most the smallest relative entropy from `Q₁` to the +null (`ProbabilityTheory.bipolarRate_le_iInf_klDiv`), the bound by that relative entropy follows +[WSJ26, Proposition 2.2, for portfolio nulls]. + +The bound in expectation, `ProbabilityTheory.IsEProcess.limsup_eintegral_log_div_le_bipolarRate` +[RR26, Lemma 3.3], holds for each `n` separately; the almost sure bound is about the whole +trajectory. + +## Main statements + +* `ProbabilityTheory.ae_limsup_log_div_le_bipolarRate_of_dependsOn`: the bound for functions `F n` + of the first `n` observations with expectation at most one under the i.i.d. laws of the null. +* `ProbabilityTheory.ae_limsup_log_div_le_bipolarRate`: the bound for `n`-sample e-variables + evaluated at the first `n` observations. +* `ProbabilityTheory.IsEProcess.ae_limsup_log_div_le_bipolarRate`: the bound for e-processes in the + filtration of the observations, per observation seen. + +## Implementation notes + +Write `d` for the bipolar rate, assume it finite, and let `L > d`. The proof has two steps. + +* **Covering.** If, almost surely, `G n ≥ exp (n L')` for infinitely many `n`, where the `G n` are + functions of the first `n` observations with expectation at most one under the null, then + `L' ≤ d`. The covering mixture of `N` observations bets half on skipping the first observation + and half on a block of the first `k` observations, with weight `1 / (k (k + 1))` and the bet + `G k`, and then continues on the remaining observations. It is a function of the first `N` + observations with expectation at most one under the null, so its expected logarithm is at most + `N d`. Parsing the observations greedily, taking a block where some `G k`, `k₀ ≤ k ≤ K`, exceeds + `exp (k L')` and skipping one observation elsewhere, bounds its logarithm from below by about + `N (L' - ε)` minus `log 2` times the number of blocks and skips. The skips are at most `K` plus + the number of positions where the shifted sequence is not good, whose mean is `N` times the + probability that no `G k` with `k₀ ≤ k ≤ K` exceeds `exp (k L')`, by stationarity; this + probability tends to `0` as `K → ∞`. +* **Zero-one law.** If `M n ≥ exp (n L)` infinitely often with positive probability, the mixture + over `s` of `M (n - s)` on the observations after the first `s`, with weights `2⁻¹ ^ (s + 1)`, + exceeds `exp (n L')` infinitely often, for `d < L' < L`, on an event that contains its preimage + under the shift. The Bernoulli shift is ergodic (Tau Ceti's + `MeasureTheory.Measure.ergodic_shift_infinitePi_const`), so this event has probability one, and + the covering step gives `L' ≤ d`, a contradiction. + +## References + +* [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1. +* [WSJ26] I. Waudby-Smith, R. Sandoval and M. I. Jordan, *Instance-log-optimality of + portfolio-based e-processes and their sequential hypothesis tests*, arXiv:2504.02818v2. +-/ + +public section + +open MeasureTheory Filter +open TauCeti.Probability (shift measurable_shift measurable_shift_iterate) +open scoped ENNReal + +namespace ProbabilityTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-! ### Shifts of an i.i.d. sequence -/ + +/-- The shift preserves the i.i.d. law. -/ +private lemma measurePreserving_shift (P : Measure 𝓧) [IsProbabilityMeasure P] : + MeasurePreserving (shift 𝓧) (Measure.infinitePi fun _ : ℕ ↦ P) + (Measure.infinitePi fun _ : ℕ ↦ P) := + (Measure.ergodic_shift_infinitePi_const P).toMeasurePreserving + +/-- The iterates of the shift preserve the i.i.d. law. -/ +private lemma measurePreserving_shift_iterate (P : Measure 𝓧) [IsProbabilityMeasure P] (t : ℕ) : + MeasurePreserving (shift 𝓧)^[t] (Measure.infinitePi fun _ : ℕ ↦ P) + (Measure.infinitePi fun _ : ℕ ↦ P) := + (measurePreserving_shift P).iterate t + +/-- Under an i.i.d. law, a function of the first `t` observations is independent of a function of +the observations after them. -/ +private lemma lintegral_mul_comp_shift_iterate (P : Measure 𝓧) [IsProbabilityMeasure P] + {f g : (ℕ → 𝓧) → ℝ≥0∞} {t : ℕ} (hf : Measurable f) (hft : DependsOn f (Set.Iio t)) + (hg : Measurable g) : + ∫⁻ ω, f ω * g ((shift 𝓧)^[t] ω) ∂Measure.infinitePi (fun _ : ℕ ↦ P) = + (∫⁻ ω, f ω ∂Measure.infinitePi (fun _ : ℕ ↦ P)) * + ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) := by + have := nonempty_of_isProbabilityMeasure P + obtain ⟨F, hF, rfl⟩ := exists_measurable_eq_comp_initSeg hf hft + -- the first `t` coordinates are independent of the later ones + have hind : IndepFun (initSeg t) (shift 𝓧)^[t] (Measure.infinitePi fun _ : ℕ ↦ P) := by + have h := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ P) (X := fun _ x ↦ x) + fun _ ↦ measurable_id).indepFun_set (Set.Iio t) (Set.Ici t) + (Set.disjoint_left.2 fun i (hi : i < t) (hi' : t ≤ i) ↦ (not_lt.2 hi') hi) + fun i ↦ measurable_pi_apply i + rw [initSeg_def, TauCeti.Probability.shift_iterate_eq_reindex] + exact h.comp (φ := fun (y : Set.Iio t → 𝓧) (i : Fin t) ↦ y ⟨i, i.2⟩) + (ψ := fun (y : Set.Ici t → 𝓧) (i : ℕ) ↦ y ⟨i + t, Nat.le_add_left t i⟩) + (by fun_prop) (by fun_prop) + rw [← (measurePreserving_shift_iterate P t).lintegral_comp hg] + exact lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun (hF.comp (measurable_initSeg t)) + (hg.comp (measurable_shift_iterate t)) (hind.comp hF hg) + +/-! ### The covering mixture -/ + +/-- The weight `1 / (k (k + 1))` of a block of `k` observations in the covering mixture. These +weights add up to at most `1`, and their logarithms are `o(k)`. -/ +private noncomputable def coverWeight (k : ℕ) : ℝ := 1 / ((k : ℝ) * (k + 1)) + +/-- The weights of the covering mixture are nonnegative. -/ +private lemma coverWeight_nonneg (k : ℕ) : 0 ≤ coverWeight k := by + unfold coverWeight + positivity + +/-- The weights of the blocks of lengths `1, …, n` add up to at most `1`. -/ +private lemma sum_coverWeight_le_one (n : ℕ) : + ∑ j ∈ Finset.range n, coverWeight (j + 1) ≤ 1 := by + have h (n : ℕ) : ∑ j ∈ Finset.range n, coverWeight (j + 1) = 1 - 1 / ((n : ℝ) + 1) := by + induction n with + | zero => simp + | succ n ih => + rw [Finset.sum_range_succ, ih, coverWeight] + push_cast + field_simp + ring + rw [h] + have : 0 ≤ 1 / ((n : ℝ) + 1) := by positivity + linarith + +/-- The logarithm of the inverse weight of a block is at most `ε` times its length, for long +blocks. -/ +private lemma exists_log_inv_coverWeight_le {ε : ℝ} (hε : 0 < ε) : + ∃ k₀ : ℕ, 1 ≤ k₀ ∧ ∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k := by + obtain ⟨x₀, hx₀⟩ := eventually_atTop.1 + (Real.isLittleO_log_id_atTop.bound (c := ε / 4) (by positivity)) + obtain ⟨k₀, hk₀⟩ := exists_nat_ge (max x₀ 1) + refine ⟨k₀, by exact_mod_cast (le_max_right _ _).trans hk₀, fun k hk ↦ ?_⟩ + have hk' : (k₀ : ℝ) ≤ k := by exact_mod_cast hk + have hk1 : (1 : ℝ) ≤ k := (le_max_right _ _).trans (hk₀.trans hk') + have hb := hx₀ ((k : ℝ) + 1) (by linarith [le_max_left x₀ 1]) + rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (Real.log_nonneg (by linarith)), id, + abs_of_nonneg (by linarith)] at hb + calc Real.log ((k : ℝ) * (k + 1)) + _ ≤ Real.log (((k : ℝ) + 1) ^ 2) := Real.log_le_log (by positivity) (by nlinarith) + _ = 2 * Real.log ((k : ℝ) + 1) := by rw [Real.log_pow]; push_cast; ring + _ ≤ ε * k := by nlinarith + +variable {M : ℕ → (ℕ → 𝓧) → ℝ≥0∞} + +variable (M) in +/-- The covering mixture of `N` observations: bet half on skipping the first observation and half +on a block of the first `k` observations, `1 ≤ k ≤ N`, with weight `coverWeight k` and the bet +`M k`; then continue on the remaining observations. -/ +private noncomputable def coverMixture (N : ℕ) (ω : ℕ → 𝓧) : ℝ≥0∞ := + match N with + | 0 => 1 + | N + 1 => 2⁻¹ * coverMixture N (shift 𝓧 ω) + 2⁻¹ * ∑ j ∈ Finset.range (N + 1), + ENNReal.ofReal (coverWeight (j + 1)) * M (j + 1) ω * + coverMixture (N - j) ((shift 𝓧)^[j + 1] ω) +termination_by N +decreasing_by all_goals omega + +/-- The covering mixture of no observation is `1`. -/ +private lemma coverMixture_zero (ω : ℕ → 𝓧) : coverMixture M 0 ω = 1 := by rw [coverMixture] + +/-- The recursive description of the covering mixture. -/ +private lemma coverMixture_succ (N : ℕ) (ω : ℕ → 𝓧) : + coverMixture M (N + 1) ω = 2⁻¹ * coverMixture M N (shift 𝓧 ω) + + 2⁻¹ * ∑ j ∈ Finset.range (N + 1), ENNReal.ofReal (coverWeight (j + 1)) * M (j + 1) ω * + coverMixture M (N - j) ((shift 𝓧)^[j + 1] ω) := by + rw [coverMixture] + +/-- The covering mixture is measurable. -/ +private lemma measurable_coverMixture (hM : ∀ n, Measurable (M n)) (N : ℕ) : + Measurable (coverMixture M N) := by + induction N using Nat.strong_induction_on with + | _ N ih => + rcases N with _ | N + · rw [funext coverMixture_zero] + exact measurable_const + · rw [funext (coverMixture_succ N)] + refine (measurable_const.mul ((ih N N.lt_succ_self).comp measurable_shift)).add + (measurable_const.mul (Finset.measurable_fun_sum _ fun j _ ↦ ?_)) + exact (measurable_const.mul (hM (j + 1))).mul + ((ih (N - j) (by omega)).comp (measurable_shift_iterate (j + 1))) + +/-- The covering mixture of `N` observations is a function of the first `N` observations. -/ +private lemma dependsOn_coverMixture (hM : ∀ n, DependsOn (M n) (Set.Iio n)) (N : ℕ) : + DependsOn (coverMixture M N) (Set.Iio N) := by + induction N using Nat.strong_induction_on with + | _ N ih => + intro ω ω' h + rcases N with _ | N + · simp only [coverMixture_zero] + rw [coverMixture_succ, coverMixture_succ, + ih N N.lt_succ_self (x := shift 𝓧 ω) (y := shift 𝓧 ω') fun i (hi : i < N) ↦ by + simpa using h (i + 1) (show i + 1 < N + 1 by omega)] + congr 2 + refine Finset.sum_congr rfl fun j hj ↦ ?_ + have hj : j < N + 1 := Finset.mem_range.1 hj + rw [hM (j + 1) fun i (hi : i < j + 1) ↦ h i (show i < N + 1 by omega), + ih (N - j) (by omega) (x := (shift 𝓧)^[j + 1] ω) (y := (shift 𝓧)^[j + 1] ω') + fun i (hi : i < N - j) ↦ by + simpa using h (i + (j + 1)) (show i + (j + 1) < N + 1 by omega)] + +/-- The covering mixture has expectation at most `1` under an i.i.d. law under which the bets +`M k` have expectation at most `1`. -/ +private lemma lintegral_coverMixture_le_one (P : Measure 𝓧) [IsProbabilityMeasure P] + (hMm : ∀ n, Measurable (M n)) (hMd : ∀ n, DependsOn (M n) (Set.Iio n)) + (hMP : ∀ n, ∫⁻ ω, M n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) (N : ℕ) : + ∫⁻ ω, coverMixture M N ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1 := by + set μ := Measure.infinitePi (fun _ : ℕ ↦ P) + have hV := measurable_coverMixture hMm + induction N using Nat.strong_induction_on with + | _ N ih => + rcases N with _ | N + · simp [coverMixture_zero] + have h2 (j : ℕ) : Measurable fun ω ↦ ENNReal.ofReal (coverWeight (j + 1)) * M (j + 1) ω * + coverMixture M (N - j) ((shift 𝓧)^[j + 1] ω) := + (measurable_const.mul (hMm (j + 1))).mul + ((hV (N - j)).comp (measurable_shift_iterate (j + 1))) + have h1 : Measurable fun ω ↦ coverMixture M N (shift 𝓧 ω) := (hV N).comp measurable_shift + simp_rw [coverMixture_succ] + rw [lintegral_add_left (f := fun ω ↦ 2⁻¹ * coverMixture M N (shift 𝓧 ω)) + (measurable_const.mul h1), + lintegral_const_mul _ h1, + lintegral_const_mul (f := fun ω ↦ ∑ j ∈ Finset.range (N + 1), + ENNReal.ofReal (coverWeight (j + 1)) * M (j + 1) ω * + coverMixture M (N - j) ((shift 𝓧)^[j + 1] ω)) _ + (Finset.measurable_fun_sum _ fun j _ ↦ h2 j), + lintegral_finsetSum _ fun j _ ↦ h2 j, (measurePreserving_shift P).lintegral_comp (hV N)] + -- each block is independent of the rest of the observations + have hsum : ∑ j ∈ Finset.range (N + 1), ∫⁻ ω, ENNReal.ofReal (coverWeight (j + 1)) * + M (j + 1) ω * coverMixture M (N - j) ((shift 𝓧)^[j + 1] ω) ∂μ ≤ 1 := by + calc ∑ j ∈ Finset.range (N + 1), ∫⁻ ω, ENNReal.ofReal (coverWeight (j + 1)) * + M (j + 1) ω * coverMixture M (N - j) ((shift 𝓧)^[j + 1] ω) ∂μ + _ = ∑ j ∈ Finset.range (N + 1), ENNReal.ofReal (coverWeight (j + 1)) * + ((∫⁻ ω, M (j + 1) ω ∂μ) * ∫⁻ ω, coverMixture M (N - j) ω ∂μ) := by + refine Finset.sum_congr rfl fun j _ ↦ ?_ + have h3 : Measurable fun ω ↦ M (j + 1) ω * coverMixture M (N - j) ((shift 𝓧)^[j + 1] ω) := + (hMm (j + 1)).mul ((hV (N - j)).comp (measurable_shift_iterate (j + 1))) + simp_rw [mul_assoc] + rw [lintegral_const_mul _ h3, + lintegral_mul_comp_shift_iterate P (hMm (j + 1)) (hMd (j + 1)) (hV (N - j))] + _ ≤ ∑ j ∈ Finset.range (N + 1), ENNReal.ofReal (coverWeight (j + 1)) := by + refine Finset.sum_le_sum fun j _ ↦ mul_le_of_le_one_right' ?_ + calc (∫⁻ ω, M (j + 1) ω ∂μ) * ∫⁻ ω, coverMixture M (N - j) ω ∂μ ≤ 1 * 1 := + mul_le_mul' (hMP _) (ih (N - j) (by omega)) + _ = 1 := one_mul 1 + _ = ENNReal.ofReal (∑ j ∈ Finset.range (N + 1), coverWeight (j + 1)) := + (ENNReal.ofReal_sum_of_nonneg fun j _ ↦ coverWeight_nonneg _).symm + _ ≤ 1 := ENNReal.ofReal_le_one.2 (sum_coverWeight_le_one (N + 1)) + calc 2⁻¹ * ∫⁻ ω, coverMixture M N ω ∂μ + 2⁻¹ * ∑ j ∈ Finset.range (N + 1), + ∫⁻ ω, ENNReal.ofReal (coverWeight (j + 1)) * M (j + 1) ω * + coverMixture M (N - j) ((shift 𝓧)^[j + 1] ω) ∂μ + _ ≤ 2⁻¹ * 1 + 2⁻¹ * 1 := by gcongr; exact ih N N.lt_succ_self + _ = 1 := by rw [mul_one, ENNReal.inv_two_add_inv_two] + +/-- The covering mixture of `N` observations is at least `2⁻¹ ^ N`. -/ +private lemma pow_le_coverMixture (N : ℕ) (ω : ℕ → 𝓧) : 2⁻¹ ^ N ≤ coverMixture M N ω := by + induction N generalizing ω with + | zero => simp [coverMixture_zero] + | succ N ih => + rw [coverMixture_succ, pow_succ'] + calc 2⁻¹ * 2⁻¹ ^ N ≤ 2⁻¹ * coverMixture M N (shift 𝓧 ω) := by gcongr; exact ih _ + _ ≤ _ := le_self_add + +/-! ### The covering argument -/ + +variable (M) in +/-- The good event of the covering argument: some bet `M k`, `k₀ ≤ k ≤ K`, is at least +`exp (k L)`. -/ +private def goodSet (L : ℝ) (k₀ K : ℕ) : Set (ℕ → 𝓧) := + {ω | ∃ k, k₀ ≤ k ∧ k ≤ K ∧ ENNReal.ofReal (Real.exp (k * L)) ≤ M k ω} + +/-- The good event is measurable. -/ +private lemma measurableSet_goodSet (hM : ∀ n, Measurable (M n)) (L : ℝ) (k₀ K : ℕ) : + MeasurableSet (goodSet M L k₀ K) := by + have : goodSet M L k₀ K = + ⋃ k ∈ Finset.Icc k₀ K, {ω | ENNReal.ofReal (Real.exp (k * L)) ≤ M k ω} := by + ext ω + simp [goodSet, and_assoc] + rw [this] + exact Finset.measurableSet_biUnion _ fun k _ ↦ measurableSet_le measurable_const (hM k) + +/-- The number of positions `s < N` at which the shifted sequence is not in `G`. -/ +private noncomputable def badCount (G : Set (ℕ → 𝓧)) (N : ℕ) (ω : ℕ → 𝓧) : ℝ := + ∑ s ∈ Finset.range N, Gᶜ.indicator 1 ((shift 𝓧)^[s] ω) + +/-- The number of bad positions is nonnegative. -/ +private lemma badCount_nonneg (G : Set (ℕ → 𝓧)) (N : ℕ) (ω : ℕ → 𝓧) : 0 ≤ badCount G N ω := + Finset.sum_nonneg fun _ _ ↦ Set.indicator_nonneg (fun _ _ ↦ zero_le_one) _ + +/-- There are at most `N` bad positions among the first `N`. -/ +private lemma badCount_le (G : Set (ℕ → 𝓧)) (N : ℕ) (ω : ℕ → 𝓧) : badCount G N ω ≤ N := by + calc badCount G N ω ≤ ∑ _s ∈ Finset.range N, (1 : ℝ) := + Finset.sum_le_sum fun _ _ ↦ Set.indicator_le_self' (fun _ _ ↦ zero_le_one) _ + _ = N := by simp + +/-- The bad positions among the first `N + 1` are the first one, if it is bad, and the bad +positions of the shifted sequence among the first `N`. -/ +private lemma badCount_succ (G : Set (ℕ → 𝓧)) (N : ℕ) (ω : ℕ → 𝓧) : + badCount G (N + 1) ω = Gᶜ.indicator 1 ω + badCount G N (shift 𝓧 ω) := by + rw [badCount, Finset.sum_range_succ', badCount, add_comm, Function.iterate_zero_apply] + simp only [Function.iterate_succ_apply] + +/-- The shifted sequence has fewer bad positions. -/ +private lemma badCount_shift_le (G : Set (ℕ → 𝓧)) {k N : ℕ} (hk : k ≤ N) (ω : ℕ → 𝓧) : + badCount G (N - k) ((shift 𝓧)^[k] ω) ≤ badCount G N ω := by + obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hk + rw [Nat.add_sub_cancel_left, badCount, badCount, Finset.sum_range_add, + Finset.sum_congr rfl fun x _ ↦ by rw [← Function.iterate_add_apply, Nat.add_comm]] + exact le_add_of_nonneg_left (badCount_nonneg G k ω) + +/-- The number of bad positions is measurable. -/ +private lemma measurable_badCount {G : Set (ℕ → 𝓧)} (hG : MeasurableSet G) (N : ℕ) : + Measurable (badCount G N) := + Finset.measurable_fun_sum _ fun s _ ↦ + (measurable_one.indicator hG.compl).comp (measurable_shift_iterate s) + +/-- The expected number of bad positions is `N` times the probability of the bad event, by +stationarity. -/ +private lemma integral_badCount (Q : Measure 𝓧) [IsProbabilityMeasure Q] {G : Set (ℕ → 𝓧)} + (hG : MeasurableSet G) (N : ℕ) : + ∫ ω, badCount G N ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q) = + N * (Measure.infinitePi (fun _ : ℕ ↦ Q)).real Gᶜ := by + set μ := Measure.infinitePi (fun _ : ℕ ↦ Q) + have hm (s : ℕ) : Measurable fun ω ↦ Gᶜ.indicator (1 : (ℕ → 𝓧) → ℝ) ((shift 𝓧)^[s] ω) := + (measurable_one.indicator hG.compl).comp (measurable_shift_iterate s) + have hi (s : ℕ) : Integrable (fun ω ↦ Gᶜ.indicator (1 : (ℕ → 𝓧) → ℝ) ((shift 𝓧)^[s] ω)) μ := + .of_bound (hm s).aestronglyMeasurable 1 (ae_of_all _ fun ω ↦ by + by_cases h : (shift 𝓧)^[s] ω ∈ G <;> simp [Set.indicator, h]) + have he (s : ℕ) : ∫ ω, Gᶜ.indicator (1 : (ℕ → 𝓧) → ℝ) ((shift 𝓧)^[s] ω) ∂μ = μ.real Gᶜ := by + rw [← integral_map (measurable_shift_iterate s).aemeasurable + (measurable_one.indicator hG.compl).aestronglyMeasurable, + (measurePreserving_shift_iterate Q s).map_eq, integral_indicator_one hG.compl] + simp only [badCount] + rw [integral_finsetSum _ fun s _ ↦ hi s, Finset.sum_congr rfl fun s _ ↦ he s] + simp + +/-- **The covering argument, pointwise.** Parse the observations greedily: at a good position, +take the block of a bet `M k ≥ exp (k L)`, `k₀ ≤ k ≤ K`; elsewhere skip one observation. Each +block of length `k` multiplies the covering mixture by at least `exp (k (L - ε)) / 2`, each skip +by `1 / 2`, and at most `N / k₀` blocks and `badCount + K` skips occur. -/ +private lemma ofReal_exp_le_coverMixture {L ε : ℝ} (hεL : ε ≤ L) {k₀ K : ℕ} (hk₀ : 1 ≤ k₀) + (hw : ∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) (N : ℕ) (ω : ℕ → 𝓧) : + ENNReal.ofReal (Real.exp ((L - ε) * (N - K - badCount (goodSet M L k₀ K) N ω) - + (N / k₀ + K + badCount (goodSet M L k₀ K) N ω) * Real.log 2)) ≤ coverMixture M N ω := by + set G := goodSet M L k₀ K + have hlog2 : 0 < Real.log 2 := Real.log_pos one_lt_two + have hk₀' : (1 : ℝ) ≤ k₀ := by exact_mod_cast hk₀ + induction N using Nat.strong_induction_on generalizing ω with + | _ N ih => + have hC := badCount_nonneg G N ω + by_cases hNK : N ≤ K + · -- too few observations: the bound is below `2⁻¹ ^ N` + refine le_trans ?_ (pow_le_coverMixture N ω) + have h2N : (2⁻¹ : ℝ≥0∞) ^ N = ENNReal.ofReal (Real.exp (-(N * Real.log 2))) := by + rw [← Real.log_pow, Real.exp_neg, Real.exp_log (by positivity), ← inv_pow, + ENNReal.ofReal_pow (by norm_num), ENNReal.ofReal_inv_of_pos two_pos, ENNReal.ofReal_ofNat] + rw [h2N] + refine ENNReal.ofReal_le_ofReal (Real.exp_le_exp.2 ?_) + have hN : (N : ℝ) ≤ K := by exact_mod_cast hNK + have h1 : (L - ε) * (N - K - badCount G N ω) ≤ 0 := + mul_nonpos_of_nonneg_of_nonpos (by linarith) (by linarith) + have h2 : (0 : ℝ) ≤ N / k₀ := by positivity + nlinarith + rw [not_le] at hNK + obtain ⟨N', rfl⟩ : ∃ N', N = N' + 1 := ⟨N - 1, by omega⟩ + by_cases hω : ω ∈ G + · -- a good position: take the block of a bet `M k ≥ exp (k L)` + obtain ⟨k, hk₀k, hkK, hkM⟩ := hω + have hk1 : 1 ≤ k := hk₀.trans hk₀k + have hkN : k ≤ N' + 1 := hkK.trans hNK.le + have hIH := ih (N' + 1 - k) (by omega) ((shift 𝓧)^[k] ω) + have hCle := badCount_shift_le G hkN ω + set C := badCount G (N' + 1) ω + set C' := badCount G (N' + 1 - k) ((shift 𝓧)^[k] ω) + set B := (L - ε) * ((N' + 1 - k : ℕ) - K - C') - + ((N' + 1 - k : ℕ) / k₀ + K + C') * Real.log 2 + have hreal : Real.exp ((L - ε) * ((N' + 1 : ℕ) - K - C) - + ((N' + 1 : ℕ) / k₀ + K + C) * Real.log 2) ≤ + 2⁻¹ * (coverWeight k * (Real.exp (k * L) * Real.exp B)) := by + have hR : 2⁻¹ * (coverWeight k * (Real.exp (k * L) * Real.exp B)) = + Real.exp (-Real.log 2 + -Real.log ((k : ℝ) * (k + 1)) + k * L + B) := by + have e1 : Real.exp (-Real.log 2) = 2⁻¹ := by rw [Real.exp_neg, Real.exp_log two_pos] + have e2 : Real.exp (-Real.log ((k : ℝ) * (k + 1))) = coverWeight k := by + rw [Real.exp_neg, Real.exp_log (by positivity), coverWeight, one_div] + rw [Real.exp_add, Real.exp_add, Real.exp_add, e1, e2] + ring + rw [hR] + refine Real.exp_le_exp.2 ?_ + have hwk := hw k hk₀k + have hq : (1 : ℝ) ≤ k / k₀ := by + rw [le_div_iff₀ (by linarith), one_mul] + exact_mod_cast hk₀k + have hsplit : ((N' + 1 : ℕ) : ℝ) / k₀ = ((N' + 1 - k : ℕ) : ℝ) / k₀ + k / k₀ := by + rw [Nat.cast_sub hkN, ← add_div] + ring + have hcast : ((N' + 1 : ℕ) : ℝ) = ((N' + 1 - k : ℕ) : ℝ) + k := by + rw [Nat.cast_sub hkN] + ring + simp only [B] + rw [hsplit, hcast] + nlinarith [mul_nonneg (sub_nonneg.2 hεL) (sub_nonneg.2 hCle), + mul_nonneg hlog2.le (sub_nonneg.2 hq), mul_nonneg hlog2.le (sub_nonneg.2 hCle)] + calc ENNReal.ofReal (Real.exp ((L - ε) * ((N' + 1 : ℕ) - K - C) - + ((N' + 1 : ℕ) / k₀ + K + C) * Real.log 2)) + _ ≤ ENNReal.ofReal (2⁻¹ * (coverWeight k * (Real.exp (k * L) * Real.exp B))) := + ENNReal.ofReal_le_ofReal hreal + _ = 2⁻¹ * (ENNReal.ofReal (coverWeight k) * (ENNReal.ofReal (Real.exp (k * L)) * + ENNReal.ofReal (Real.exp B))) := by + rw [ENNReal.ofReal_mul (by norm_num), ENNReal.ofReal_mul (coverWeight_nonneg k), + ENNReal.ofReal_mul (Real.exp_pos _).le, ENNReal.ofReal_inv_of_pos two_pos, + ENNReal.ofReal_ofNat] + _ ≤ 2⁻¹ * (ENNReal.ofReal (coverWeight k) * + (M k ω * coverMixture M (N' + 1 - k) ((shift 𝓧)^[k] ω))) := by + gcongr + _ ≤ 2⁻¹ * ∑ j ∈ Finset.range (N' + 1), ENNReal.ofReal (coverWeight (j + 1)) * + M (j + 1) ω * coverMixture M (N' - j) ((shift 𝓧)^[j + 1] ω) := by + gcongr + have h := Finset.single_le_sum (f := fun j ↦ ENNReal.ofReal (coverWeight (j + 1)) * + M (j + 1) ω * coverMixture M (N' - j) ((shift 𝓧)^[j + 1] ω)) (fun _ _ ↦ bot_le) + (Finset.mem_range.2 (show k - 1 < N' + 1 by omega)) + have e1 : k - 1 + 1 = k := by omega + have e2 : N' - (k - 1) = N' + 1 - k := by omega + simp only [e1, e2] at h + rw [← mul_assoc] + exact h + _ ≤ coverMixture M (N' + 1) ω := by + rw [coverMixture_succ] + exact le_add_self + · -- a bad position: skip one observation + have hIH := ih N' N'.lt_succ_self (shift 𝓧 ω) + have hCsucc := badCount_succ G N' ω + rw [Set.indicator_of_mem (show ω ∈ Gᶜ from hω), Pi.one_apply] at hCsucc + set C'' := badCount G N' (shift 𝓧 ω) + have hreal : Real.exp ((L - ε) * ((N' + 1 : ℕ) - K - badCount G (N' + 1) ω) - + ((N' + 1 : ℕ) / k₀ + K + badCount G (N' + 1) ω) * Real.log 2) ≤ + 2⁻¹ * Real.exp ((L - ε) * (N' - K - C'') - (N' / k₀ + K + C'') * Real.log 2) := by + rw [show (2⁻¹ : ℝ) = Real.exp (-Real.log 2) by rw [Real.exp_neg, Real.exp_log two_pos], + ← Real.exp_add] + refine Real.exp_le_exp.2 ?_ + rw [hCsucc] + push_cast + have : (N' : ℝ) / k₀ + 1 / k₀ = (N' + 1) / k₀ := by ring + have h1k : (0 : ℝ) ≤ 1 / k₀ := by positivity + nlinarith + calc ENNReal.ofReal (Real.exp ((L - ε) * ((N' + 1 : ℕ) - K - badCount G (N' + 1) ω) - + ((N' + 1 : ℕ) / k₀ + K + badCount G (N' + 1) ω) * Real.log 2)) + _ ≤ ENNReal.ofReal (2⁻¹ * Real.exp ((L - ε) * (N' - K - C'') - + (N' / k₀ + K + C'') * Real.log 2)) := ENNReal.ofReal_le_ofReal hreal + _ = 2⁻¹ * ENNReal.ofReal (Real.exp ((L - ε) * (N' - K - C'') - + (N' / k₀ + K + C'') * Real.log 2)) := by + rw [ENNReal.ofReal_mul (by norm_num), ENNReal.ofReal_inv_of_pos two_pos, + ENNReal.ofReal_ofNat] + _ ≤ 2⁻¹ * coverMixture M N' (shift 𝓧 ω) := by gcongr + _ ≤ coverMixture M (N' + 1) ω := by + rw [coverMixture_succ] + exact le_self_add + +/-- **The covering argument.** Let `M n` be functions of the first `n` observations with +expectation at most `1` under the i.i.d. laws of the members of `S`. If, almost surely under the +i.i.d. law of `Q`, `M n ≥ exp (n L)` for infinitely many `n`, then `L` is at most the bipolar rate: +the covering mixture of `N` observations has expected logarithm at least about +`N ((L - ε) (1 - q) - (1 / k₀ + q) log 2)`, where `q` is the probability that no bet `M k`, +`k₀ ≤ k ≤ K`, exceeds `exp (k L)`, and at most `N` times the bipolar rate. -/ +private lemma coe_le_bipolarRate_of_ae_frequently (Q : Measure 𝓧) [IsProbabilityMeasure Q] + {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hMm : ∀ n, Measurable (M n)) (hMd : ∀ n, DependsOn (M n) (Set.Iio n)) + (hMS : ∀ P ∈ S, ∀ n, ∫⁻ ω, M n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) {L : ℝ} + (hL : ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q), + ∃ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (n * L)) ≤ M n ω) : + (L : EReal) ≤ bipolarRate Q S := by + set μ := Measure.infinitePi (fun _ : ℕ ↦ Q) + by_cases hd : bipolarRate Q S = ⊤ + · rw [hd] + exact le_top + set d := (bipolarRate Q S).toReal + have hdeq : (d : EReal) = bipolarRate Q S := + EReal.coe_toReal hd (ne_bot_of_le_ne_bot EReal.zero_ne_bot (bipolarRate_nonneg Q S)) + rw [← hdeq, EReal.coe_le_coe_iff] + by_cases hL0 : L ≤ 0 + · exact hL0.trans (EReal.toReal_nonneg (bipolarRate_nonneg Q S)) + rw [not_le] at hL0 + have hlog2 : 0 < Real.log 2 := Real.log_pos one_lt_two + -- the bound for fixed `ε`, `k₀` and `K` + have step1 : ∀ ε : ℝ, 0 < ε → ε ≤ L → ∀ k₀ : ℕ, 1 ≤ k₀ → + (∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) → ∀ K : ℕ, + (L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * μ.real (goodSet M L k₀ K)ᶜ ≤ d := by + intro ε hε hεL k₀ hk₀ hw K + set G := goodSet M L k₀ K + set q := μ.real Gᶜ + have hG := measurableSet_goodSet hMm L k₀ K + have hN : ∀ N : ℕ, 1 ≤ N → + (L - ε) * (N - K - N * q) - (N / k₀ + K + N * q) * Real.log 2 ≤ N * d := by + intro N hN1 + have hbi : Integrable (badCount G N) μ := + .of_bound (measurable_badCount hG N).aestronglyMeasurable N (ae_of_all _ fun ω ↦ by + rw [Real.norm_eq_abs, abs_of_nonneg (badCount_nonneg G N ω)] + exact badCount_le G N ω) + have hA : Integrable (fun ω ↦ (L - ε) * (N - K - badCount G N ω)) μ := + ((integrable_const _).sub hbi).const_mul _ + have hB : Integrable (fun ω ↦ (N / k₀ + K + badCount G N ω) * Real.log 2) μ := + ((integrable_const _).add hbi).mul_const _ + have hAB : Integrable (fun ω ↦ (L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2) μ := hA.sub hB + have hval : ∫ ω, ((L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2) ∂μ = + (L - ε) * (N - K - N * q) - (N / k₀ + K + N * q) * Real.log 2 := by + rw [integral_sub hA hB, integral_const_mul, integral_mul_const, + integral_sub (integrable_const _) hbi, integral_add (integrable_const _) hbi, + integral_badCount Q hG N] + simp only [integral_const, probReal_univ, one_smul] + rfl + have hle : (((L - ε) * (N - K - N * q) - (N / k₀ + K + N * q) * Real.log 2 : ℝ) : + EReal) ≤ N * bipolarRate Q S := by + rw [← hval, ← eintegral_eq_integral hAB] + calc ∫ᵉ ω, (((L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2 : ℝ) : EReal) ∂μ + _ ≤ ∫ᵉ ω, ENNReal.log (coverMixture M N ω) ∂μ := eintegral_mono fun ω ↦ by + rw [← Real.log_exp ((L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2), + ← ENNReal.log_ofReal_of_pos (Real.exp_pos _)] + exact ENNReal.log_le_log (ofReal_exp_le_coverMixture hεL hk₀ hw N ω) + _ ≤ maxLogGrowth Q S N := + eintegral_log_le_maxLogGrowth_of_dependsOn Q hS (measurable_coverMixture hMm N) + (dependsOn_coverMixture hMd N) fun P hP ↦ by + have := hS P hP + exact lintegral_coverMixture_le_one P hMm hMd (hMS P hP) N + _ ≤ N * bipolarRate Q S := maxLogGrowth_le_mul_bipolarRate Q S (by omega) + rwa [← hdeq, ← EReal.coe_natCast, ← EReal.coe_mul, EReal.coe_le_coe_iff] at hle + -- let `N → ∞` + by_contra hcon + rw [not_le] at hcon + set δ := (L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * q - d with hδ + have hδ0 : 0 < δ := by linarith + obtain ⟨N, hN'⟩ := exists_nat_gt (K * (L - ε + Real.log 2) / δ) + have h := hN (N + 1) (by omega) + rw [div_lt_iff₀ hδ0] at hN' + have hk₀' : (0 : ℝ) < k₀ := by exact_mod_cast hk₀ + have hsplit : (((N + 1 : ℕ) : ℝ)) / k₀ = ((N + 1 : ℕ) : ℝ) * (1 / k₀) := by ring + rw [hsplit] at h + have : ((N + 1 : ℕ) : ℝ) * δ ≤ K * (L - ε + Real.log 2) := by + rw [hδ] + have : Real.log 2 / k₀ = Real.log 2 * (1 / k₀) := by ring + rw [this] + nlinarith + push_cast at this + nlinarith + -- as `K → ∞`, the probability of the bad event tends to `0` + have step2 (k₀ : ℕ) : Tendsto (fun K : ℕ ↦ μ.real (goodSet M L k₀ K)ᶜ) atTop (nhds 0) := by + have hanti : Antitone fun K : ℕ ↦ (goodSet M L k₀ K)ᶜ := fun K K' hKK' ω hω hω' ↦ by + obtain ⟨k, hk₀k, hkK, hkM⟩ := hω' + exact hω ⟨k, hk₀k, hkK.trans hKK', hkM⟩ + have hinter : μ (⋂ K : ℕ, (goodSet M L k₀ K)ᶜ) = 0 := by + refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.1 hL) + simp only [Set.mem_iInter, Set.mem_compl_iff] at hω + intro hfreq + obtain ⟨k, hk, hkM⟩ := (frequently_atTop.1 hfreq) k₀ + exact hω k ⟨k, hk, le_rfl, hkM⟩ + have h := tendsto_measure_iInter_atTop (μ := μ) + (fun K ↦ (measurableSet_goodSet hMm L k₀ K).compl.nullMeasurableSet) hanti + ⟨0, measure_ne_top _ _⟩ + rw [hinter] at h + simpa [Function.comp_def, measureReal_def] using + (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h + -- let `K → ∞` + have step3 : ∀ ε : ℝ, 0 < ε → ε ≤ L → ∀ k₀ : ℕ, 1 ≤ k₀ → + (∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) → + (L - ε) - Real.log 2 / k₀ ≤ d := by + intro ε hε hεL k₀ hk₀ hw + have hlim : Tendsto (fun K : ℕ ↦ (L - ε) - Real.log 2 / k₀ - + (L - ε + Real.log 2) * μ.real (goodSet M L k₀ K)ᶜ) atTop + (nhds ((L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * 0)) := + tendsto_const_nhds.sub (tendsto_const_nhds.mul (step2 k₀)) + rw [mul_zero, sub_zero] at hlim + exact le_of_tendsto' hlim fun K ↦ step1 ε hε hεL k₀ hk₀ hw K + -- let `ε → 0` and `k₀ → ∞` + refine le_of_forall_pos_le_add fun η hη ↦ ?_ + set ε := min (η / 2) L + have hε : 0 < ε := lt_min (by linarith) hL0 + obtain ⟨k₀, hk₀, hw⟩ := exists_log_inv_coverWeight_le hε + obtain ⟨k₁, hk₁⟩ := exists_nat_gt (Real.log 2 / (η / 2)) + have hk : 1 ≤ max k₀ k₁ := hk₀.trans (le_max_left _ _) + have h := step3 ε hε (min_le_right _ _) (max k₀ k₁) hk + fun k hk' ↦ hw k ((le_max_left _ _).trans hk') + have hk₁' : (k₁ : ℝ) ≤ max k₀ k₁ := by exact_mod_cast le_max_right k₀ k₁ + have hpos : (0 : ℝ) < max k₀ k₁ := by exact_mod_cast hk + have hdiv : Real.log 2 / (max k₀ k₁ : ℕ) ≤ η / 2 := by + rw [div_le_iff₀ hpos] + rw [div_lt_iff₀ (by linarith)] at hk₁ + push_cast at hpos hk₁' ⊢ + nlinarith + have hεη : ε ≤ η / 2 := min_le_left _ _ + linarith + +/-! ### The mixture over shifts -/ + +variable (M) in +/-- The mixture over `s < n` of the functions `M (n - s)` of the observations after the first +`s`, with weights `2⁻¹ ^ (s + 1)`. -/ +private noncomputable def shiftMixture (n : ℕ) (ω : ℕ → 𝓧) : ℝ≥0∞ := + ∑ s ∈ Finset.range n, 2⁻¹ ^ (s + 1) * M (n - s) ((shift 𝓧)^[s] ω) + +/-- The shift mixture is measurable. -/ +private lemma measurable_shiftMixture (hM : ∀ n, Measurable (M n)) (n : ℕ) : + Measurable (shiftMixture M n) := + Finset.measurable_fun_sum _ fun s _ ↦ measurable_const.mul + ((hM (n - s)).comp (measurable_shift_iterate s)) + +/-- The shift mixture of functions of the first observations is a function of the first `n` +observations. -/ +private lemma dependsOn_shiftMixture (hM : ∀ n, DependsOn (M n) (Set.Iio n)) (n : ℕ) : + DependsOn (shiftMixture M n) (Set.Iio n) := by + intro ω ω' h + refine Finset.sum_congr rfl fun s hs ↦ ?_ + rw [hM (n - s) fun i (hi : i < n - s) ↦ ?_] + simpa using h (i + s) (show i + s < n by omega) + +/-- The shift mixture of functions with expectation at most `1` under an i.i.d. law has +expectation at most `1`. -/ +private lemma lintegral_shiftMixture_le_one (P : Measure 𝓧) [IsProbabilityMeasure P] + (hMm : ∀ n, Measurable (M n)) + (hMP : ∀ n, ∫⁻ ω, M n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) (n : ℕ) : + ∫⁻ ω, shiftMixture M n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1 := by + have hm (s : ℕ) : Measurable fun ω ↦ M (n - s) ((shift 𝓧)^[s] ω) := + (hMm (n - s)).comp (measurable_shift_iterate s) + have hm' (s : ℕ) : Measurable fun ω ↦ 2⁻¹ ^ (s + 1) * M (n - s) ((shift 𝓧)^[s] ω) := + measurable_const.mul (hm s) + simp only [shiftMixture] + rw [lintegral_finsetSum _ fun s _ ↦ hm' s] + calc ∑ s ∈ Finset.range n, ∫⁻ ω, 2⁻¹ ^ (s + 1) * M (n - s) ((shift 𝓧)^[s] ω) + ∂Measure.infinitePi (fun _ : ℕ ↦ P) + _ = ∑ s ∈ Finset.range n, 2⁻¹ ^ (s + 1) * + ∫⁻ ω, M (n - s) ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) := by + refine Finset.sum_congr rfl fun s _ ↦ ?_ + rw [lintegral_const_mul _ (hm s), + (measurePreserving_shift_iterate P s).lintegral_comp (hMm (n - s))] + _ ≤ ∑ s ∈ Finset.range n, (2⁻¹ : ℝ≥0∞) ^ (s + 1) := + Finset.sum_le_sum fun s _ ↦ mul_le_of_le_one_right' (hMP _) + _ ≤ ∑' s, (2⁻¹ : ℝ≥0∞) ^ (s + 1) := sum_le_tsum _ + _ = 1 := by + simp_rw [pow_succ', ENNReal.tsum_mul_left, ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, + inv_inv] + exact ENNReal.inv_mul_cancel (by simp) (by simp) + +/-- If `M m ≥ exp (m L)` for infinitely many `m` along the shifted sequence, then the shift +mixture exceeds `exp (n L')` for infinitely many `n`, for every `L' < L`. -/ +private lemma frequently_le_shiftMixture {L L' : ℝ} (hLL' : L' < L) {s : ℕ} {ω : ℕ → 𝓧} + (h : ∃ᶠ m : ℕ in atTop, ENNReal.ofReal (Real.exp (m * L)) ≤ M m ((shift 𝓧)^[s] ω)) : + ∃ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (n * L')) ≤ shiftMixture M n ω := by + obtain ⟨m₀, hm₀⟩ := exists_nat_gt ((s * L' + (s + 1) * Real.log 2) / (L - L')) + rw [frequently_atTop] at h ⊢ + intro a + obtain ⟨m, hm, hmL⟩ := h (max a m₀ + 1) + refine ⟨m + s, by omega, ?_⟩ + have hm1 : (m₀ : ℝ) < m := by exact_mod_cast (by omega : m₀ < m) + have hreal : Real.exp (((m + s : ℕ) : ℝ) * L') ≤ (1 / 2) ^ (s + 1) * Real.exp (m * L) := by + rw [show ((1 : ℝ) / 2) ^ (s + 1) = Real.exp (-((s + 1) * Real.log 2)) by + rw [Real.exp_neg, show ((s : ℝ) + 1) * Real.log 2 = Real.log (2 ^ (s + 1)) by + rw [Real.log_pow]; push_cast; ring, Real.exp_log (by positivity), one_div, inv_pow], + ← Real.exp_add] + refine Real.exp_le_exp.2 ?_ + rw [div_lt_iff₀ (by linarith)] at hm₀ + push_cast + nlinarith + calc ENNReal.ofReal (Real.exp (((m + s : ℕ) : ℝ) * L')) + _ ≤ ENNReal.ofReal ((1 / 2) ^ (s + 1) * Real.exp (m * L)) := ENNReal.ofReal_le_ofReal hreal + _ = 2⁻¹ ^ (s + 1) * ENNReal.ofReal (Real.exp (m * L)) := by + rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_pow (by norm_num), + ENNReal.ofReal_div_of_pos zero_lt_two, ENNReal.ofReal_one, ENNReal.ofReal_ofNat, one_div] + _ ≤ 2⁻¹ ^ (s + 1) * M m ((shift 𝓧)^[s] ω) := by gcongr + _ = 2⁻¹ ^ (s + 1) * M (m + s - s) ((shift 𝓧)^[s] ω) := by rw [Nat.add_sub_cancel] + _ ≤ shiftMixture M (m + s) ω := + Finset.single_le_sum (f := fun s' ↦ 2⁻¹ ^ (s' + 1) * M (m + s - s') ((shift 𝓧)^[s'] ω)) + (fun _ _ ↦ bot_le) (Finset.mem_range.2 (by omega)) + +/-! ### The almost sure growth bound -/ + +variable {Q₁ : Measure 𝓧} {S₁ : Set (Measure 𝓧)} + +/-- **No function of the first observations grows faster than the bipolar rate, almost surely.** +Let `F n` be measurable functions of the first `n` observations with expectation at most `1` +under the i.i.d. laws of the members of `S₁`. Almost surely under the i.i.d. law of `Q₁`, +`limsup (1/n) log (F n) ≤ bipolarRate Q₁ S₁`. If `Q₁` is not a probability measure, its i.i.d. +law `Measure.infinitePi` is `0` and the statement holds trivially. -/ +theorem ae_limsup_log_div_le_bipolarRate_of_dependsOn (Q₁ : Measure 𝓧) + (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) {F : ℕ → (ℕ → 𝓧) → ℝ≥0∞} + (hF : ∀ n, Measurable (F n)) (hFn : ∀ n, DependsOn (F n) (Set.Iio n)) + (h_null : ∀ P ∈ S₁, ∀ n, ∫⁻ ω, F n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) : + ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁), + limsup (fun n : ℕ ↦ ENNReal.log (F n ω) / (n : EReal)) atTop ≤ bipolarRate Q₁ S₁ := by + by_cases hQ : IsProbabilityMeasure Q₁ + swap + · simp [Measure.infinitePi, hQ] + set μ := Measure.infinitePi (fun _ : ℕ ↦ Q₁) + by_cases hd : bipolarRate Q₁ S₁ = ⊤ + · simp [hd] + set d := (bipolarRate Q₁ S₁).toReal + have hdeq : (d : EReal) = bipolarRate Q₁ S₁ := + EReal.coe_toReal hd (ne_bot_of_le_ne_bot EReal.zero_ne_bot (bipolarRate_nonneg Q₁ S₁)) + -- for `L > d`, almost surely `F n < exp (n L)` eventually + have key (L : ℝ) (hL : d < L) : + ∀ᵐ ω ∂μ, ∀ᶠ n : ℕ in atTop, F n ω < ENNReal.ofReal (Real.exp (n * L)) := by + set B := {ω | ∃ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (n * L)) ≤ F n ω} + have hBm : MeasurableSet B := by + have : B = ⋂ N : ℕ, ⋃ n ≥ N, {ω | ENNReal.ofReal (Real.exp (n * L)) ≤ F n ω} := by + ext ω + simp [B, frequently_atTop] + rw [this] + exact .iInter fun N ↦ .iUnion fun n ↦ .iUnion fun _ ↦ + measurableSet_le measurable_const (hF n) + have hB : μ B = 0 → ∀ᵐ ω ∂μ, ∀ᶠ n : ℕ in atTop, + F n ω < ENNReal.ofReal (Real.exp (n * L)) := fun h0 ↦ + ae_iff.2 (measure_mono_null (fun ω hω ↦ by + simp only [Set.mem_ofPred_eq, not_eventually, not_lt] at hω + exact hω) h0) + -- the event that some shifted sequence is in `B` has probability `0` or `1` + set U := ⋃ s, (shift 𝓧)^[s] ⁻¹' B + have hUm : MeasurableSet U := .iUnion fun s ↦ measurable_shift_iterate s hBm + have hBU : B ⊆ U := fun ω hω ↦ Set.mem_iUnion.2 ⟨0, hω⟩ + have hUshift : shift 𝓧 ⁻¹' U ⊆ U := fun ω hω ↦ by + obtain ⟨s, hs⟩ := Set.mem_iUnion.1 hω + exact Set.mem_iUnion.2 ⟨s + 1, by rwa [Set.mem_preimage, Function.iterate_succ_apply]⟩ + rcases (Measure.ergodic_shift_infinitePi_const Q₁).ae_empty_or_univ_of_preimage_ae_le + hUm.nullMeasurableSet (ae_of_all _ fun ω (hω : ω ∈ shift 𝓧 ⁻¹' U) ↦ hUshift hω) + with hU | hU + · exact hB (measure_mono_null hBU (ae_eq_empty.1 hU)) + -- if it has probability `1`, the shift mixture grows at a rate above `d` + have hUae : ∀ᵐ ω ∂μ, ω ∈ U := by + rw [ae_iff] + exact ae_eq_univ.1 hU + have hae : ∀ᵐ ω ∂μ, ∃ᶠ n : ℕ in atTop, + ENNReal.ofReal (Real.exp (n * ((d + L) / 2))) ≤ shiftMixture F n ω := by + filter_upwards [hUae] with ω hω + obtain ⟨s, hs⟩ := Set.mem_iUnion.1 hω + exact frequently_le_shiftMixture (by linarith) hs + have h := coe_le_bipolarRate_of_ae_frequently Q₁ hS₁ (measurable_shiftMixture hF) + (dependsOn_shiftMixture hFn) (fun P hP n ↦ by + have := hS₁ P hP + exact lintegral_shiftMixture_le_one P hF (h_null P hP) n) hae + rw [← hdeq, EReal.coe_le_coe_iff] at h + linarith + have key' : ∀ᵐ ω ∂μ, ∀ k : ℕ, ∀ᶠ n in atTop, + F n ω < ENNReal.ofReal (Real.exp (n * (d + 1 / ((k : ℝ) + 1)))) := + ae_all_iff.2 fun k ↦ key _ (lt_add_of_pos_right _ (by positivity)) + filter_upwards [key'] with ω hω + refine le_of_forall_gt_imp_ge_of_dense fun c hc ↦ ?_ + induction c using EReal.rec with + | bot => exact absurd hc not_lt_bot + | top => exact le_top + | coe c => + rw [← hdeq, EReal.coe_lt_coe_iff] at hc + obtain ⟨k, hk⟩ := exists_nat_one_div_lt (sub_pos.2 hc) + refine limsup_le_of_le (by isBoundedDefault) (((hω k).and (eventually_ge_atTop 1)).mono + fun n hn ↦ ?_) + obtain ⟨hn, hn1⟩ := hn + rw [EReal.div_le_iff_le_mul (by exact_mod_cast hn1) (EReal.natCast_ne_top n)] + calc ENNReal.log (F n ω) + _ ≤ ENNReal.log (ENNReal.ofReal (Real.exp (n * (d + 1 / ((k : ℝ) + 1))))) := + ENNReal.log_le_log hn.le + _ = ((n * (d + 1 / ((k : ℝ) + 1)) : ℝ) : EReal) := by + rw [ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp] + _ ≤ n * c := by + rw [← EReal.coe_natCast, ← EReal.coe_mul, EReal.coe_le_coe_iff] + exact mul_le_mul_of_nonneg_left (by linarith) (Nat.cast_nonneg n) + +/-- **No sequence of `n`-sample e-variables grows faster than the bipolar rate, almost surely.** +For every sequence of `n`-sample e-variables `M n` for the i.i.d. laws of the members of `S₁`, +almost surely under the i.i.d. law of `Q₁`, `M n` evaluated at the first `n` observations has +`limsup (1/n) log (M n) ≤ bipolarRate Q₁ S₁`. -/ +theorem ae_limsup_log_div_le_bipolarRate (Q₁ : Measure 𝓧) + (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) {M : (n : ℕ) → (Fin n → 𝓧) → ℝ≥0∞} + (hM : ∀ n, IsEVar (M n) ((fun P ↦ Measure.pi fun _ : Fin n ↦ P) '' S₁)) : + ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁), + limsup (fun n : ℕ ↦ ENNReal.log (M n (initSeg n ω)) / (n : EReal)) atTop ≤ + bipolarRate Q₁ S₁ := + ae_limsup_log_div_le_bipolarRate_of_dependsOn Q₁ hS₁ (F := fun n ω ↦ M n (initSeg n ω)) + (fun n ↦ (hM n).measurable.comp (measurable_initSeg n)) + (fun n ↦ dependsOn_comp_initSeg (M n)) fun P hP n ↦ by + have := hS₁ P hP + rw [(measurePreserving_initSeg P n).lintegral_comp (hM n).measurable] + exact (hM n).lintegral_le_one ⟨P, hP, rfl⟩ + +/-- **No e-process for an i.i.d. null grows faster than the bipolar rate, almost surely.** For an +e-process `E` for the i.i.d. laws of the members of `S₁`, in the filtration of the observations, +almost surely under the i.i.d. law of `Q₁`, the logarithm of `E n` divided by the number `n + 1` of +observations it has seen has `limsup` at most `bipolarRate Q₁ S₁`. -/ +theorem IsEProcess.ae_limsup_log_div_le_bipolarRate (Q₁ : Measure 𝓧) + (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) {E : ℕ → (ℕ → 𝓧) → ℝ≥0∞} + (hE : IsEProcess E (Filtration.piLE (X := fun _ : ℕ ↦ 𝓧)) + ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁)) : + ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁), + limsup (fun n : ℕ ↦ ENNReal.log (E n ω) / ((n + 1 : ℕ) : EReal)) atTop ≤ + bipolarRate Q₁ S₁ := by + -- at time `n` the process has seen `n + 1` observations: start the sequence with `1` + set F : ℕ → (ℕ → 𝓧) → ℝ≥0∞ := fun n ω ↦ if n = 0 then 1 else E (n - 1) ω + have hF : ∀ n, Measurable (F n) := by + rintro (_ | n) + · simp [F] + · simpa [F] using hE.measurable n + have hFn : ∀ n, DependsOn (F n) (Set.Iio n) := by + rintro (_ | n) ω ω' h + · simp [F] + · simpa [F] using (hE.adapted n).dependsOn_of_piLE + fun i hi ↦ h i (Nat.lt_succ_of_le (Set.mem_Iic.1 hi)) + have h_null : ∀ P ∈ S₁, ∀ n, ∫⁻ ω, F n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1 := by + rintro P hP (_ | n) + · have := hS₁ P hP + simp [F] + · have := hS₁ P hP + simpa [F] using (hE.isEVar n).lintegral_le_one ⟨P, hP, rfl⟩ + filter_upwards [ae_limsup_log_div_le_bipolarRate_of_dependsOn Q₁ hS₁ hF hFn h_null] with ω hω + rw [← limsup_nat_add _ 1] at hω + simpa [F] using hω + +end ProbabilityTheory From 0e5f6bc5df7c56c737594b4039c27ada853a93be Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 16:45:53 +0100 Subject: [PATCH 2/2] refactor: export the i.i.d. shift lemmas and split the covering argument Move measurePreserving_shift, measurePreserving_shift_iterate and lintegral_mul_comp_shift_iterate to LMLExplore/Probability/ProductMeasure.lean as public lemmas, add Measure.infinitePi_eq_zero_of_not_isProbabilityMeasure, credit the paper project's source file, fix the citation of the per-n expectation bound, and split the long covering proofs into private lemmas. Co-Authored-By: Claude Code --- .../EValues/BipolarRate/AlmostSure.lean | 362 +++++++++--------- LMLExplore/Probability/ProductMeasure.lean | 61 ++- 2 files changed, 241 insertions(+), 182 deletions(-) diff --git a/LMLExplore/EValues/BipolarRate/AlmostSure.lean b/LMLExplore/EValues/BipolarRate/AlmostSure.lean index 1caebead..ffb25e39 100644 --- a/LMLExplore/EValues/BipolarRate/AlmostSure.lean +++ b/LMLExplore/EValues/BipolarRate/AlmostSure.lean @@ -6,8 +6,6 @@ Authors: LMLExplore contributors module public import LMLExplore.EValues.BipolarRate.EProcess -import Mathlib.Probability.Independence.Integration -import TauCeti.Probability.Ergodic.BernoulliShift /-! # E-processes for an i.i.d. null grow at most at the bipolar rate, almost surely @@ -23,7 +21,7 @@ or compactness. Since the bipolar rate is at most the smallest relative entropy null (`ProbabilityTheory.bipolarRate_le_iInf_klDiv`), the bound by that relative entropy follows [WSJ26, Proposition 2.2, for portfolio nulls]. -The bound in expectation, `ProbabilityTheory.IsEProcess.limsup_eintegral_log_div_le_bipolarRate` +The bound in expectation, `ProbabilityTheory.IsEProcess.eintegral_log_div_le_bipolarRate` [RR26, Lemma 3.3], holds for each `n` separately; the almost sure bound is about the whole trajectory. @@ -59,6 +57,10 @@ Write `d` for the bipolar rate, assume it finite, and let `L > d`. The proof has `MeasureTheory.Measure.ergodic_shift_infinitePi_const`), so this event has probability one, and the covering step gives `L' ≤ d`, a contradiction. +The statements and proofs are adapted from `EValuesResearch/Results/BipolarRate.lean` +(commit `decbae4`) in the paper project `RemyDegenne/evalues_research` (same author), rewritten on +the API of LMLExplore. + ## References * [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1. @@ -76,44 +78,6 @@ namespace ProbabilityTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} -/-! ### Shifts of an i.i.d. sequence -/ - -/-- The shift preserves the i.i.d. law. -/ -private lemma measurePreserving_shift (P : Measure 𝓧) [IsProbabilityMeasure P] : - MeasurePreserving (shift 𝓧) (Measure.infinitePi fun _ : ℕ ↦ P) - (Measure.infinitePi fun _ : ℕ ↦ P) := - (Measure.ergodic_shift_infinitePi_const P).toMeasurePreserving - -/-- The iterates of the shift preserve the i.i.d. law. -/ -private lemma measurePreserving_shift_iterate (P : Measure 𝓧) [IsProbabilityMeasure P] (t : ℕ) : - MeasurePreserving (shift 𝓧)^[t] (Measure.infinitePi fun _ : ℕ ↦ P) - (Measure.infinitePi fun _ : ℕ ↦ P) := - (measurePreserving_shift P).iterate t - -/-- Under an i.i.d. law, a function of the first `t` observations is independent of a function of -the observations after them. -/ -private lemma lintegral_mul_comp_shift_iterate (P : Measure 𝓧) [IsProbabilityMeasure P] - {f g : (ℕ → 𝓧) → ℝ≥0∞} {t : ℕ} (hf : Measurable f) (hft : DependsOn f (Set.Iio t)) - (hg : Measurable g) : - ∫⁻ ω, f ω * g ((shift 𝓧)^[t] ω) ∂Measure.infinitePi (fun _ : ℕ ↦ P) = - (∫⁻ ω, f ω ∂Measure.infinitePi (fun _ : ℕ ↦ P)) * - ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) := by - have := nonempty_of_isProbabilityMeasure P - obtain ⟨F, hF, rfl⟩ := exists_measurable_eq_comp_initSeg hf hft - -- the first `t` coordinates are independent of the later ones - have hind : IndepFun (initSeg t) (shift 𝓧)^[t] (Measure.infinitePi fun _ : ℕ ↦ P) := by - have h := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ P) (X := fun _ x ↦ x) - fun _ ↦ measurable_id).indepFun_set (Set.Iio t) (Set.Ici t) - (Set.disjoint_left.2 fun i (hi : i < t) (hi' : t ≤ i) ↦ (not_lt.2 hi') hi) - fun i ↦ measurable_pi_apply i - rw [initSeg_def, TauCeti.Probability.shift_iterate_eq_reindex] - exact h.comp (φ := fun (y : Set.Iio t → 𝓧) (i : Fin t) ↦ y ⟨i, i.2⟩) - (ψ := fun (y : Set.Ici t → 𝓧) (i : ℕ) ↦ y ⟨i + t, Nat.le_add_left t i⟩) - (by fun_prop) (by fun_prop) - rw [← (measurePreserving_shift_iterate P t).lintegral_comp hg] - exact lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun (hF.comp (measurable_initSeg t)) - (hg.comp (measurable_shift_iterate t)) (hind.comp hF hg) - /-! ### The covering mixture -/ /-- The weight `1 / (k (k + 1))` of a block of `k` observations in the covering mixture. These @@ -158,6 +122,21 @@ private lemma exists_log_inv_coverWeight_le {ε : ℝ} (hε : 0 < ε) : _ = 2 * Real.log ((k : ℝ) + 1) := by rw [Real.log_pow]; push_cast; ring _ ≤ ε * k := by nlinarith +/-- `2⁻¹ ^ n` is `exp (-(n log 2))`. -/ +private lemma inv_two_pow_eq_exp (n : ℕ) : (2⁻¹ : ℝ) ^ n = Real.exp (-(n * Real.log 2)) := by + rw [← Real.log_pow, Real.exp_neg, Real.exp_log (by positivity), inv_pow] + +/-- `2⁻¹ ^ n` is `exp (-(n log 2))`, in `ℝ≥0∞`. -/ +private lemma inv_two_pow_eq_ofReal_exp (n : ℕ) : + (2⁻¹ : ℝ≥0∞) ^ n = ENNReal.ofReal (Real.exp (-(n * Real.log 2))) := by + rw [← inv_two_pow_eq_exp, ENNReal.ofReal_pow (by norm_num), ENNReal.ofReal_inv_of_pos two_pos, + ENNReal.ofReal_ofNat] + +/-- A finite bipolar rate is the coercion of its real value. -/ +private lemma coe_toReal_bipolarRate {Q : Measure 𝓧} {S : Set (Measure 𝓧)} + (hd : bipolarRate Q S ≠ ⊤) : ((bipolarRate Q S).toReal : EReal) = bipolarRate Q S := + EReal.coe_toReal hd (ne_bot_of_le_ne_bot EReal.zero_ne_bot (bipolarRate_nonneg Q S)) + variable {M : ℕ → (ℕ → 𝓧) → ℝ≥0∞} variable (M) in @@ -351,6 +330,29 @@ private lemma integral_badCount (Q : Measure 𝓧) [IsProbabilityMeasure Q] {G : rw [integral_finsetSum _ fun s _ ↦ hi s, Finset.sum_congr rfl fun s _ ↦ he s] simp +/-- The exponent of the pointwise covering bound at a good position: taking a block of length +`k ≥ k₀`, of weight `exp (-w)` with `w ≤ ε k`, and of bet at least `exp (k L)`, with a factor +`exp (-l)` for the choice of a block, loses no more than the bound allows. -/ +private lemma cover_exponent_le_of_good {L ε k k₀ K n C C' w l : ℝ} (hεL : ε ≤ L) (hl : 0 < l) + (hk₀ : 0 < k₀) (hkk₀ : k₀ ≤ k) (hw : w ≤ ε * k) (hC : C' ≤ C) : + (L - ε) * (n + k - K - C) - ((n + k) / k₀ + K + C) * l ≤ + -l + -w + k * L + ((L - ε) * (n - K - C') - (n / k₀ + K + C') * l) := by + have hq : 1 ≤ k / k₀ := by rwa [le_div_iff₀ hk₀, one_mul] + have hsplit : (n + k) / k₀ = n / k₀ + k / k₀ := add_div _ _ _ + rw [hsplit] + nlinarith [mul_nonneg (sub_nonneg.2 hεL) (sub_nonneg.2 hC), mul_nonneg hl.le (sub_nonneg.2 hq), + mul_nonneg hl.le (sub_nonneg.2 hC)] + +/-- The exponent of the pointwise covering bound at a bad position: skipping one observation, with +a factor `exp (-l)`, loses no more than the bound allows. -/ +private lemma cover_exponent_le_of_bad {L ε k₀ K n C l : ℝ} (hl : 0 < l) (hk₀ : 0 < k₀) : + (L - ε) * (n + 1 - K - (1 + C)) - ((n + 1) / k₀ + K + (1 + C)) * l ≤ + -l + ((L - ε) * (n - K - C) - (n / k₀ + K + C) * l) := by + have h : (n + 1) / k₀ = n / k₀ + 1 / k₀ := add_div _ _ _ + have h1k : 0 ≤ 1 / k₀ := by positivity + rw [h] + nlinarith [mul_nonneg hl.le h1k] + /-- **The covering argument, pointwise.** Parse the observations greedily: at a good position, take the block of a bet `M k ≥ exp (k L)`, `k₀ ≤ k ≤ K`; elsewhere skip one observation. Each block of length `k` multiplies the covering mixture by at least `exp (k (L - ε)) / 2`, each skip @@ -361,17 +363,16 @@ private lemma ofReal_exp_le_coverMixture {L ε : ℝ} (hεL : ε ≤ L) {k₀ K (N / k₀ + K + badCount (goodSet M L k₀ K) N ω) * Real.log 2)) ≤ coverMixture M N ω := by set G := goodSet M L k₀ K have hlog2 : 0 < Real.log 2 := Real.log_pos one_lt_two - have hk₀' : (1 : ℝ) ≤ k₀ := by exact_mod_cast hk₀ + have hk₀' : (0 : ℝ) < k₀ := by exact_mod_cast hk₀ + have hexp2 : Real.exp (-Real.log 2) = 2⁻¹ := by + rw [← pow_one (2⁻¹ : ℝ), inv_two_pow_eq_exp, Nat.cast_one, one_mul] induction N using Nat.strong_induction_on generalizing ω with | _ N ih => have hC := badCount_nonneg G N ω by_cases hNK : N ≤ K · -- too few observations: the bound is below `2⁻¹ ^ N` refine le_trans ?_ (pow_le_coverMixture N ω) - have h2N : (2⁻¹ : ℝ≥0∞) ^ N = ENNReal.ofReal (Real.exp (-(N * Real.log 2))) := by - rw [← Real.log_pow, Real.exp_neg, Real.exp_log (by positivity), ← inv_pow, - ENNReal.ofReal_pow (by norm_num), ENNReal.ofReal_inv_of_pos two_pos, ENNReal.ofReal_ofNat] - rw [h2N] + rw [inv_two_pow_eq_ofReal_exp] refine ENNReal.ofReal_le_ofReal (Real.exp_le_exp.2 ?_) have hN : (N : ℝ) ≤ K := by exact_mod_cast hNK have h1 : (L - ε) * (N - K - badCount G N ω) ≤ 0 := @@ -383,10 +384,9 @@ private lemma ofReal_exp_le_coverMixture {L ε : ℝ} (hεL : ε ≤ L) {k₀ K by_cases hω : ω ∈ G · -- a good position: take the block of a bet `M k ≥ exp (k L)` obtain ⟨k, hk₀k, hkK, hkM⟩ := hω - have hk1 : 1 ≤ k := hk₀.trans hk₀k + have hk1 : 0 < k := hk₀.trans hk₀k have hkN : k ≤ N' + 1 := hkK.trans hNK.le have hIH := ih (N' + 1 - k) (by omega) ((shift 𝓧)^[k] ω) - have hCle := badCount_shift_le G hkN ω set C := badCount G (N' + 1) ω set C' := badCount G (N' + 1 - k) ((shift 𝓧)^[k] ω) set B := (L - ε) * ((N' + 1 - k : ℕ) - K - C') - @@ -396,27 +396,16 @@ private lemma ofReal_exp_le_coverMixture {L ε : ℝ} (hεL : ε ≤ L) {k₀ K 2⁻¹ * (coverWeight k * (Real.exp (k * L) * Real.exp B)) := by have hR : 2⁻¹ * (coverWeight k * (Real.exp (k * L) * Real.exp B)) = Real.exp (-Real.log 2 + -Real.log ((k : ℝ) * (k + 1)) + k * L + B) := by - have e1 : Real.exp (-Real.log 2) = 2⁻¹ := by rw [Real.exp_neg, Real.exp_log two_pos] have e2 : Real.exp (-Real.log ((k : ℝ) * (k + 1))) = coverWeight k := by rw [Real.exp_neg, Real.exp_log (by positivity), coverWeight, one_div] - rw [Real.exp_add, Real.exp_add, Real.exp_add, e1, e2] - ring - rw [hR] - refine Real.exp_le_exp.2 ?_ - have hwk := hw k hk₀k - have hq : (1 : ℝ) ≤ k / k₀ := by - rw [le_div_iff₀ (by linarith), one_mul] - exact_mod_cast hk₀k - have hsplit : ((N' + 1 : ℕ) : ℝ) / k₀ = ((N' + 1 - k : ℕ) : ℝ) / k₀ + k / k₀ := by - rw [Nat.cast_sub hkN, ← add_div] + rw [Real.exp_add, Real.exp_add, Real.exp_add, hexp2, e2] ring have hcast : ((N' + 1 : ℕ) : ℝ) = ((N' + 1 - k : ℕ) : ℝ) + k := by rw [Nat.cast_sub hkN] ring - simp only [B] - rw [hsplit, hcast] - nlinarith [mul_nonneg (sub_nonneg.2 hεL) (sub_nonneg.2 hCle), - mul_nonneg hlog2.le (sub_nonneg.2 hq), mul_nonneg hlog2.le (sub_nonneg.2 hCle)] + rw [hR, hcast] + exact Real.exp_le_exp.2 (cover_exponent_le_of_good hεL hlog2 hk₀' + (by exact_mod_cast hk₀k) (hw k hk₀k) (badCount_shift_le G hkN ω)) calc ENNReal.ofReal (Real.exp ((L - ε) * ((N' + 1 : ℕ) - K - C) - ((N' + 1 : ℕ) / k₀ + K + C) * Real.log 2)) _ ≤ ENNReal.ofReal (2⁻¹ * (coverWeight k * (Real.exp (k * L) * Real.exp B))) := @@ -451,14 +440,8 @@ private lemma ofReal_exp_le_coverMixture {L ε : ℝ} (hεL : ε ≤ L) {k₀ K have hreal : Real.exp ((L - ε) * ((N' + 1 : ℕ) - K - badCount G (N' + 1) ω) - ((N' + 1 : ℕ) / k₀ + K + badCount G (N' + 1) ω) * Real.log 2) ≤ 2⁻¹ * Real.exp ((L - ε) * (N' - K - C'') - (N' / k₀ + K + C'') * Real.log 2) := by - rw [show (2⁻¹ : ℝ) = Real.exp (-Real.log 2) by rw [Real.exp_neg, Real.exp_log two_pos], - ← Real.exp_add] - refine Real.exp_le_exp.2 ?_ - rw [hCsucc] - push_cast - have : (N' : ℝ) / k₀ + 1 / k₀ = (N' + 1) / k₀ := by ring - have h1k : (0 : ℝ) ≤ 1 / k₀ := by positivity - nlinarith + rw [← hexp2, ← Real.exp_add, hCsucc, Nat.cast_succ] + exact Real.exp_le_exp.2 (cover_exponent_le_of_bad hlog2 hk₀') calc ENNReal.ofReal (Real.exp ((L - ε) * ((N' + 1 : ℕ) - K - badCount G (N' + 1) ω) - ((N' + 1 : ℕ) / k₀ + K + badCount G (N' + 1) ω) * Real.log 2)) _ ≤ ENNReal.ofReal (2⁻¹ * Real.exp ((L - ε) * (N' - K - C'') - @@ -472,6 +455,125 @@ private lemma ofReal_exp_le_coverMixture {L ε : ℝ} (hεL : ε ≤ L) {k₀ K rw [coverMixture_succ] exact le_self_add +/-- **The covering argument, for fixed `N`.** Integrating the pointwise bound +`ofReal_exp_le_coverMixture`, where the expected number of bad positions is `N q` with `q` the +probability of the bad event, gives a lower bound on the expected logarithm of the covering +mixture, which is at most `N` times the bipolar rate. -/ +private lemma cover_le_mul_toReal_bipolarRate (Q : Measure 𝓧) [IsProbabilityMeasure Q] + {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hMm : ∀ n, Measurable (M n)) (hMd : ∀ n, DependsOn (M n) (Set.Iio n)) + (hMS : ∀ P ∈ S, ∀ n, ∫⁻ ω, M n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) + (hd : bipolarRate Q S ≠ ⊤) {L ε : ℝ} (hεL : ε ≤ L) {k₀ : ℕ} (hk₀ : 1 ≤ k₀) + (hw : ∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) (K : ℕ) {N : ℕ} (hN : 1 ≤ N) : + (L - ε) * (N - K - N * (Measure.infinitePi fun _ : ℕ ↦ Q).real (goodSet M L k₀ K)ᶜ) - + (N / k₀ + K + N * (Measure.infinitePi fun _ : ℕ ↦ Q).real (goodSet M L k₀ K)ᶜ) * + Real.log 2 ≤ N * (bipolarRate Q S).toReal := by + set μ := Measure.infinitePi (fun _ : ℕ ↦ Q) + set G := goodSet M L k₀ K + have hG := measurableSet_goodSet hMm L k₀ K + have hbi : Integrable (badCount G N) μ := + .of_bound (measurable_badCount hG N).aestronglyMeasurable N (ae_of_all _ fun ω ↦ by + rw [Real.norm_eq_abs, abs_of_nonneg (badCount_nonneg G N ω)] + exact badCount_le G N ω) + have hA : Integrable (fun ω ↦ (L - ε) * (N - K - badCount G N ω)) μ := + ((integrable_const _).sub hbi).const_mul _ + have hB : Integrable (fun ω ↦ (N / k₀ + K + badCount G N ω) * Real.log 2) μ := + ((integrable_const _).add hbi).mul_const _ + have hAB : Integrable (fun ω ↦ (L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2) μ := hA.sub hB + have hval : ∫ ω, ((L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2) ∂μ = + (L - ε) * (N - K - N * μ.real Gᶜ) - (N / k₀ + K + N * μ.real Gᶜ) * Real.log 2 := by + rw [integral_sub hA hB, integral_const_mul, integral_mul_const, + integral_sub (integrable_const _) hbi, integral_add (integrable_const _) hbi, + integral_badCount Q hG N] + simp only [integral_const, probReal_univ, one_smul, μ, G] + have hle : (((L - ε) * (N - K - N * μ.real Gᶜ) - (N / k₀ + K + N * μ.real Gᶜ) * Real.log 2 : + ℝ) : EReal) ≤ N * bipolarRate Q S := by + rw [← hval, ← eintegral_eq_integral hAB] + calc ∫ᵉ ω, (((L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2 : ℝ) : EReal) ∂μ + _ ≤ ∫ᵉ ω, ENNReal.log (coverMixture M N ω) ∂μ := eintegral_mono fun ω ↦ by + rw [← Real.log_exp ((L - ε) * (N - K - badCount G N ω) - + (N / k₀ + K + badCount G N ω) * Real.log 2), + ← ENNReal.log_ofReal_of_pos (Real.exp_pos _)] + exact ENNReal.log_le_log (ofReal_exp_le_coverMixture hεL hk₀ hw N ω) + _ ≤ maxLogGrowth Q S N := + eintegral_log_le_maxLogGrowth_of_dependsOn Q hS (measurable_coverMixture hMm N) + (dependsOn_coverMixture hMd N) fun P hP ↦ by + have := hS P hP + exact lintegral_coverMixture_le_one P hMm hMd (hMS P hP) N + _ ≤ N * bipolarRate Q S := maxLogGrowth_le_mul_bipolarRate Q S (by omega) + rwa [← coe_toReal_bipolarRate hd, ← EReal.coe_natCast, ← EReal.coe_mul, + EReal.coe_le_coe_iff] at hle + +/-- If `N a - b ≤ N d` for every `N ≥ 1`, then `a ≤ d`. -/ +private lemma le_of_forall_mul_sub_le {a b d : ℝ} (h : ∀ N : ℕ, 1 ≤ N → N * a - b ≤ N * d) : + a ≤ d := by + by_contra hcon + rw [not_le] at hcon + obtain ⟨N, hN⟩ := exists_nat_gt (b / (a - d)) + have h1 := h (N + 1) (by omega) + rw [div_lt_iff₀ (by linarith)] at hN + push_cast at h1 + nlinarith + +/-- **The covering argument, for fixed `K`.** Letting `N → ∞` in +`cover_le_mul_toReal_bipolarRate`. -/ +private lemma sub_le_toReal_bipolarRate_of_goodSet (Q : Measure 𝓧) [IsProbabilityMeasure Q] + {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hMm : ∀ n, Measurable (M n)) (hMd : ∀ n, DependsOn (M n) (Set.Iio n)) + (hMS : ∀ P ∈ S, ∀ n, ∫⁻ ω, M n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) + (hd : bipolarRate Q S ≠ ⊤) {L ε : ℝ} (hεL : ε ≤ L) {k₀ : ℕ} (hk₀ : 1 ≤ k₀) + (hw : ∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) (K : ℕ) : + (L - ε) - Real.log 2 / k₀ - + (L - ε + Real.log 2) * (Measure.infinitePi fun _ : ℕ ↦ Q).real (goodSet M L k₀ K)ᶜ ≤ + (bipolarRate Q S).toReal := by + refine le_of_forall_mul_sub_le (b := K * (L - ε + Real.log 2)) fun N hN ↦ ?_ + refine le_of_eq_of_le ?_ (cover_le_mul_toReal_bipolarRate Q hS hMm hMd hMS hd hεL hk₀ hw K hN) + ring + +/-- As `K → ∞`, the probability that no bet `M k`, `k₀ ≤ k ≤ K`, exceeds `exp (k L)` tends to `0` +when, almost surely, `M n ≥ exp (n L)` for infinitely many `n`. -/ +private lemma tendsto_measureReal_compl_goodSet {μ : Measure (ℕ → 𝓧)} [IsFiniteMeasure μ] + (hMm : ∀ n, Measurable (M n)) {L : ℝ} + (hL : ∀ᵐ ω ∂μ, ∃ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (n * L)) ≤ M n ω) (k₀ : ℕ) : + Tendsto (fun K : ℕ ↦ μ.real (goodSet M L k₀ K)ᶜ) atTop (nhds 0) := by + have hanti : Antitone fun K : ℕ ↦ (goodSet M L k₀ K)ᶜ := fun K K' hKK' ω hω hω' ↦ by + obtain ⟨k, hk₀k, hkK, hkM⟩ := hω' + exact hω ⟨k, hk₀k, hkK.trans hKK', hkM⟩ + have hinter : μ (⋂ K : ℕ, (goodSet M L k₀ K)ᶜ) = 0 := by + refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.1 hL) + simp only [Set.mem_iInter, Set.mem_compl_iff] at hω + intro hfreq + obtain ⟨k, hk, hkM⟩ := (frequently_atTop.1 hfreq) k₀ + exact hω k ⟨k, hk, le_rfl, hkM⟩ + have h := tendsto_measure_iInter_atTop (μ := μ) + (fun K ↦ (measurableSet_goodSet hMm L k₀ K).compl.nullMeasurableSet) hanti + ⟨0, measure_ne_top _ _⟩ + rw [hinter] at h + simpa [Function.comp_def, measureReal_def] using + (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h + +/-- **The covering argument, for fixed `ε` and `k₀`.** Letting `K → ∞` in +`sub_le_toReal_bipolarRate_of_goodSet`. -/ +private lemma sub_log_two_div_le_toReal_bipolarRate (Q : Measure 𝓧) [IsProbabilityMeasure Q] + {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hMm : ∀ n, Measurable (M n)) (hMd : ∀ n, DependsOn (M n) (Set.Iio n)) + (hMS : ∀ P ∈ S, ∀ n, ∫⁻ ω, M n ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) + (hd : bipolarRate Q S ≠ ⊤) {L : ℝ} + (hL : ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q), + ∃ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (n * L)) ≤ M n ω) {ε : ℝ} (hεL : ε ≤ L) + {k₀ : ℕ} (hk₀ : 1 ≤ k₀) (hw : ∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) : + (L - ε) - Real.log 2 / k₀ ≤ (bipolarRate Q S).toReal := by + have hlim : Tendsto (fun K : ℕ ↦ (L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * + (Measure.infinitePi fun _ : ℕ ↦ Q).real (goodSet M L k₀ K)ᶜ) atTop + (nhds ((L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * 0)) := + tendsto_const_nhds.sub (tendsto_const_nhds.mul (tendsto_measureReal_compl_goodSet hMm hL k₀)) + rw [mul_zero, sub_zero] at hlim + exact le_of_tendsto' hlim + (sub_le_toReal_bipolarRate_of_goodSet Q hS hMm hMd hMS hd hεL hk₀ hw) + /-- **The covering argument.** Let `M n` be functions of the first `n` observations with expectation at most `1` under the i.i.d. laws of the members of `S`. If, almost surely under the i.i.d. law of `Q`, `M n ≥ exp (n L)` for infinitely many `n`, then `L` is at most the bipolar rate: @@ -485,110 +587,13 @@ private lemma coe_le_bipolarRate_of_ae_frequently (Q : Measure 𝓧) [IsProbabil (hL : ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q), ∃ᶠ n : ℕ in atTop, ENNReal.ofReal (Real.exp (n * L)) ≤ M n ω) : (L : EReal) ≤ bipolarRate Q S := by - set μ := Measure.infinitePi (fun _ : ℕ ↦ Q) by_cases hd : bipolarRate Q S = ⊤ · rw [hd] exact le_top - set d := (bipolarRate Q S).toReal - have hdeq : (d : EReal) = bipolarRate Q S := - EReal.coe_toReal hd (ne_bot_of_le_ne_bot EReal.zero_ne_bot (bipolarRate_nonneg Q S)) - rw [← hdeq, EReal.coe_le_coe_iff] + rw [← coe_toReal_bipolarRate hd, EReal.coe_le_coe_iff] by_cases hL0 : L ≤ 0 · exact hL0.trans (EReal.toReal_nonneg (bipolarRate_nonneg Q S)) rw [not_le] at hL0 - have hlog2 : 0 < Real.log 2 := Real.log_pos one_lt_two - -- the bound for fixed `ε`, `k₀` and `K` - have step1 : ∀ ε : ℝ, 0 < ε → ε ≤ L → ∀ k₀ : ℕ, 1 ≤ k₀ → - (∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) → ∀ K : ℕ, - (L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * μ.real (goodSet M L k₀ K)ᶜ ≤ d := by - intro ε hε hεL k₀ hk₀ hw K - set G := goodSet M L k₀ K - set q := μ.real Gᶜ - have hG := measurableSet_goodSet hMm L k₀ K - have hN : ∀ N : ℕ, 1 ≤ N → - (L - ε) * (N - K - N * q) - (N / k₀ + K + N * q) * Real.log 2 ≤ N * d := by - intro N hN1 - have hbi : Integrable (badCount G N) μ := - .of_bound (measurable_badCount hG N).aestronglyMeasurable N (ae_of_all _ fun ω ↦ by - rw [Real.norm_eq_abs, abs_of_nonneg (badCount_nonneg G N ω)] - exact badCount_le G N ω) - have hA : Integrable (fun ω ↦ (L - ε) * (N - K - badCount G N ω)) μ := - ((integrable_const _).sub hbi).const_mul _ - have hB : Integrable (fun ω ↦ (N / k₀ + K + badCount G N ω) * Real.log 2) μ := - ((integrable_const _).add hbi).mul_const _ - have hAB : Integrable (fun ω ↦ (L - ε) * (N - K - badCount G N ω) - - (N / k₀ + K + badCount G N ω) * Real.log 2) μ := hA.sub hB - have hval : ∫ ω, ((L - ε) * (N - K - badCount G N ω) - - (N / k₀ + K + badCount G N ω) * Real.log 2) ∂μ = - (L - ε) * (N - K - N * q) - (N / k₀ + K + N * q) * Real.log 2 := by - rw [integral_sub hA hB, integral_const_mul, integral_mul_const, - integral_sub (integrable_const _) hbi, integral_add (integrable_const _) hbi, - integral_badCount Q hG N] - simp only [integral_const, probReal_univ, one_smul] - rfl - have hle : (((L - ε) * (N - K - N * q) - (N / k₀ + K + N * q) * Real.log 2 : ℝ) : - EReal) ≤ N * bipolarRate Q S := by - rw [← hval, ← eintegral_eq_integral hAB] - calc ∫ᵉ ω, (((L - ε) * (N - K - badCount G N ω) - - (N / k₀ + K + badCount G N ω) * Real.log 2 : ℝ) : EReal) ∂μ - _ ≤ ∫ᵉ ω, ENNReal.log (coverMixture M N ω) ∂μ := eintegral_mono fun ω ↦ by - rw [← Real.log_exp ((L - ε) * (N - K - badCount G N ω) - - (N / k₀ + K + badCount G N ω) * Real.log 2), - ← ENNReal.log_ofReal_of_pos (Real.exp_pos _)] - exact ENNReal.log_le_log (ofReal_exp_le_coverMixture hεL hk₀ hw N ω) - _ ≤ maxLogGrowth Q S N := - eintegral_log_le_maxLogGrowth_of_dependsOn Q hS (measurable_coverMixture hMm N) - (dependsOn_coverMixture hMd N) fun P hP ↦ by - have := hS P hP - exact lintegral_coverMixture_le_one P hMm hMd (hMS P hP) N - _ ≤ N * bipolarRate Q S := maxLogGrowth_le_mul_bipolarRate Q S (by omega) - rwa [← hdeq, ← EReal.coe_natCast, ← EReal.coe_mul, EReal.coe_le_coe_iff] at hle - -- let `N → ∞` - by_contra hcon - rw [not_le] at hcon - set δ := (L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * q - d with hδ - have hδ0 : 0 < δ := by linarith - obtain ⟨N, hN'⟩ := exists_nat_gt (K * (L - ε + Real.log 2) / δ) - have h := hN (N + 1) (by omega) - rw [div_lt_iff₀ hδ0] at hN' - have hk₀' : (0 : ℝ) < k₀ := by exact_mod_cast hk₀ - have hsplit : (((N + 1 : ℕ) : ℝ)) / k₀ = ((N + 1 : ℕ) : ℝ) * (1 / k₀) := by ring - rw [hsplit] at h - have : ((N + 1 : ℕ) : ℝ) * δ ≤ K * (L - ε + Real.log 2) := by - rw [hδ] - have : Real.log 2 / k₀ = Real.log 2 * (1 / k₀) := by ring - rw [this] - nlinarith - push_cast at this - nlinarith - -- as `K → ∞`, the probability of the bad event tends to `0` - have step2 (k₀ : ℕ) : Tendsto (fun K : ℕ ↦ μ.real (goodSet M L k₀ K)ᶜ) atTop (nhds 0) := by - have hanti : Antitone fun K : ℕ ↦ (goodSet M L k₀ K)ᶜ := fun K K' hKK' ω hω hω' ↦ by - obtain ⟨k, hk₀k, hkK, hkM⟩ := hω' - exact hω ⟨k, hk₀k, hkK.trans hKK', hkM⟩ - have hinter : μ (⋂ K : ℕ, (goodSet M L k₀ K)ᶜ) = 0 := by - refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.1 hL) - simp only [Set.mem_iInter, Set.mem_compl_iff] at hω - intro hfreq - obtain ⟨k, hk, hkM⟩ := (frequently_atTop.1 hfreq) k₀ - exact hω k ⟨k, hk, le_rfl, hkM⟩ - have h := tendsto_measure_iInter_atTop (μ := μ) - (fun K ↦ (measurableSet_goodSet hMm L k₀ K).compl.nullMeasurableSet) hanti - ⟨0, measure_ne_top _ _⟩ - rw [hinter] at h - simpa [Function.comp_def, measureReal_def] using - (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h - -- let `K → ∞` - have step3 : ∀ ε : ℝ, 0 < ε → ε ≤ L → ∀ k₀ : ℕ, 1 ≤ k₀ → - (∀ k : ℕ, k₀ ≤ k → Real.log ((k : ℝ) * (k + 1)) ≤ ε * k) → - (L - ε) - Real.log 2 / k₀ ≤ d := by - intro ε hε hεL k₀ hk₀ hw - have hlim : Tendsto (fun K : ℕ ↦ (L - ε) - Real.log 2 / k₀ - - (L - ε + Real.log 2) * μ.real (goodSet M L k₀ K)ᶜ) atTop - (nhds ((L - ε) - Real.log 2 / k₀ - (L - ε + Real.log 2) * 0)) := - tendsto_const_nhds.sub (tendsto_const_nhds.mul (step2 k₀)) - rw [mul_zero, sub_zero] at hlim - exact le_of_tendsto' hlim fun K ↦ step1 ε hε hεL k₀ hk₀ hw K -- let `ε → 0` and `k₀ → ∞` refine le_of_forall_pos_le_add fun η hη ↦ ?_ set ε := min (η / 2) L @@ -596,7 +601,7 @@ private lemma coe_le_bipolarRate_of_ae_frequently (Q : Measure 𝓧) [IsProbabil obtain ⟨k₀, hk₀, hw⟩ := exists_log_inv_coverWeight_le hε obtain ⟨k₁, hk₁⟩ := exists_nat_gt (Real.log 2 / (η / 2)) have hk : 1 ≤ max k₀ k₁ := hk₀.trans (le_max_left _ _) - have h := step3 ε hε (min_le_right _ _) (max k₀ k₁) hk + have h := sub_log_two_div_le_toReal_bipolarRate Q hS hMm hMd hMS hd hL (min_le_right _ _) hk fun k hk' ↦ hw k ((le_max_left _ _).trans hk') have hk₁' : (k₁ : ℝ) ≤ max k₀ k₁ := by exact_mod_cast le_max_right k₀ k₁ have hpos : (0 : ℝ) < max k₀ k₁ := by exact_mod_cast hk @@ -669,20 +674,16 @@ private lemma frequently_le_shiftMixture {L L' : ℝ} (hLL' : L' < L) {s : ℕ} obtain ⟨m, hm, hmL⟩ := h (max a m₀ + 1) refine ⟨m + s, by omega, ?_⟩ have hm1 : (m₀ : ℝ) < m := by exact_mod_cast (by omega : m₀ < m) - have hreal : Real.exp (((m + s : ℕ) : ℝ) * L') ≤ (1 / 2) ^ (s + 1) * Real.exp (m * L) := by - rw [show ((1 : ℝ) / 2) ^ (s + 1) = Real.exp (-((s + 1) * Real.log 2)) by - rw [Real.exp_neg, show ((s : ℝ) + 1) * Real.log 2 = Real.log (2 ^ (s + 1)) by - rw [Real.log_pow]; push_cast; ring, Real.exp_log (by positivity), one_div, inv_pow], - ← Real.exp_add] + have hreal : Real.exp (((m + s : ℕ) : ℝ) * L') ≤ 2⁻¹ ^ (s + 1) * Real.exp (m * L) := by + rw [inv_two_pow_eq_exp, ← Real.exp_add] refine Real.exp_le_exp.2 ?_ rw [div_lt_iff₀ (by linarith)] at hm₀ push_cast nlinarith calc ENNReal.ofReal (Real.exp (((m + s : ℕ) : ℝ) * L')) - _ ≤ ENNReal.ofReal ((1 / 2) ^ (s + 1) * Real.exp (m * L)) := ENNReal.ofReal_le_ofReal hreal + _ ≤ ENNReal.ofReal (2⁻¹ ^ (s + 1) * Real.exp (m * L)) := ENNReal.ofReal_le_ofReal hreal _ = 2⁻¹ ^ (s + 1) * ENNReal.ofReal (Real.exp (m * L)) := by - rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_pow (by norm_num), - ENNReal.ofReal_div_of_pos zero_lt_two, ENNReal.ofReal_one, ENNReal.ofReal_ofNat, one_div] + rw [ENNReal.ofReal_mul (by positivity), inv_two_pow_eq_exp, ← inv_two_pow_eq_ofReal_exp] _ ≤ 2⁻¹ ^ (s + 1) * M m ((shift 𝓧)^[s] ω) := by gcongr _ = 2⁻¹ ^ (s + 1) * M (m + s - s) ((shift 𝓧)^[s] ω) := by rw [Nat.add_sub_cancel] _ ≤ shiftMixture M (m + s) ω := @@ -706,13 +707,12 @@ theorem ae_limsup_log_div_le_bipolarRate_of_dependsOn (Q₁ : Measure 𝓧) limsup (fun n : ℕ ↦ ENNReal.log (F n ω) / (n : EReal)) atTop ≤ bipolarRate Q₁ S₁ := by by_cases hQ : IsProbabilityMeasure Q₁ swap - · simp [Measure.infinitePi, hQ] + · simp [Measure.infinitePi_eq_zero_of_not_isProbabilityMeasure (μ := fun _ : ℕ ↦ Q₁) (i := 0) hQ] set μ := Measure.infinitePi (fun _ : ℕ ↦ Q₁) by_cases hd : bipolarRate Q₁ S₁ = ⊤ · simp [hd] set d := (bipolarRate Q₁ S₁).toReal - have hdeq : (d : EReal) = bipolarRate Q₁ S₁ := - EReal.coe_toReal hd (ne_bot_of_le_ne_bot EReal.zero_ne_bot (bipolarRate_nonneg Q₁ S₁)) + have hdeq : (d : EReal) = bipolarRate Q₁ S₁ := coe_toReal_bipolarRate hd -- for `L > d`, almost surely `F n < exp (n L)` eventually have key (L : ℝ) (hL : d < L) : ∀ᵐ ω ∂μ, ∀ᶠ n : ℕ in atTop, F n ω < ENNReal.ofReal (Real.exp (n * L)) := by diff --git a/LMLExplore/Probability/ProductMeasure.lean b/LMLExplore/Probability/ProductMeasure.lean index c218f9e8..2ee5f5a1 100644 --- a/LMLExplore/Probability/ProductMeasure.lean +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -7,13 +7,16 @@ module public import LMLExplore.MeasureTheory.MeasurableSpace.Constructions public import Mathlib.Probability.Independence.InfinitePi +public import TauCeti.Probability.Ergodic.BernoulliShift +import Mathlib.Probability.Independence.Integration /-! # Infinite products of probability measures: the first terms and the next terms Under the infinite product `Measure.infinitePi` of copies of a probability measure `μ`, the first `n` coordinates have the product law `Measure.pi`, and they are independent of the next `m` -coordinates. +coordinates. The shift of an i.i.d. sequence is again i.i.d. with the same law, and a function of +the first `t` terms is independent of a function of the terms after them. ## Main statements @@ -21,10 +24,18 @@ coordinates. have the product law. * `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the first `n` terms and the next `m` terms are independent. +* `MeasureTheory.measurePreserving_shift`, `MeasureTheory.measurePreserving_shift_iterate`: the + shift and its iterates preserve the i.i.d. law. +* `MeasureTheory.lintegral_mul_comp_shift_iterate`: under an i.i.d. law, a function of the first + `t` terms is independent of a function of the terms after them. +* `MeasureTheory.Measure.infinitePi_eq_zero_of_not_isProbabilityMeasure`: the infinite product + is `0` as soon as one factor is not a probability measure. -/ public section +open scoped ENNReal + namespace MeasureTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} @@ -37,10 +48,58 @@ lemma measurePreserving_initSeg (P : Measure 𝓧) [IsProbabilityMeasure P] (n : rw [initSeg_def, ← Measure.infinitePi_eq_pi] exact Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective +open TauCeti.Probability (shift measurable_shift_iterate) + +/-- The shift preserves the i.i.d. law. -/ +lemma measurePreserving_shift (P : Measure 𝓧) [IsProbabilityMeasure P] : + MeasurePreserving (shift 𝓧) (Measure.infinitePi fun _ : ℕ ↦ P) + (Measure.infinitePi fun _ : ℕ ↦ P) := + (Measure.ergodic_shift_infinitePi_const P).toMeasurePreserving + +/-- The iterates of the shift preserve the i.i.d. law. -/ +lemma measurePreserving_shift_iterate (P : Measure 𝓧) [IsProbabilityMeasure P] (t : ℕ) : + MeasurePreserving (shift 𝓧)^[t] (Measure.infinitePi fun _ : ℕ ↦ P) + (Measure.infinitePi fun _ : ℕ ↦ P) := + (measurePreserving_shift P).iterate t + +open ProbabilityTheory in +/-- Under an i.i.d. law, a function of the first `t` terms is independent of a function of the +terms after them: the expectation of their product is the product of their expectations. -/ +lemma lintegral_mul_comp_shift_iterate (P : Measure 𝓧) [IsProbabilityMeasure P] + {f g : (ℕ → 𝓧) → ℝ≥0∞} {t : ℕ} (hf : Measurable f) (hft : DependsOn f (Set.Iio t)) + (hg : Measurable g) : + ∫⁻ ω, f ω * g ((shift 𝓧)^[t] ω) ∂Measure.infinitePi (fun _ : ℕ ↦ P) = + (∫⁻ ω, f ω ∂Measure.infinitePi (fun _ : ℕ ↦ P)) * + ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) := by + have := nonempty_of_isProbabilityMeasure P + obtain ⟨F, hF, rfl⟩ := exists_measurable_eq_comp_initSeg hf hft + -- the first `t` coordinates are independent of the later ones + have hind : IndepFun (initSeg t) (shift 𝓧)^[t] (Measure.infinitePi fun _ : ℕ ↦ P) := by + have h := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ P) (X := fun _ x ↦ x) + fun _ ↦ measurable_id).indepFun_set (Set.Iio t) (Set.Ici t) + (Set.disjoint_left.2 fun i (hi : i < t) (hi' : t ≤ i) ↦ (not_lt.2 hi') hi) + fun i ↦ measurable_pi_apply i + rw [initSeg_def, TauCeti.Probability.shift_iterate_eq_reindex] + exact h.comp (φ := fun (y : Set.Iio t → 𝓧) (i : Fin t) ↦ y ⟨i, i.2⟩) + (ψ := fun (y : Set.Ici t → 𝓧) (i : ℕ) ↦ y ⟨i + t, Nat.le_add_left t i⟩) + (by fun_prop) (by fun_prop) + rw [← (measurePreserving_shift_iterate P t).lintegral_comp hg] + exact lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun (hF.comp (measurable_initSeg t)) + (hg.comp (measurable_shift_iterate t)) (hind.comp hF hg) + end MeasureTheory namespace MeasureTheory.Measure +/-- The infinite product of a family of measures is `0` as soon as one of them is not a probability +measure. -/ +lemma infinitePi_eq_zero_of_not_isProbabilityMeasure {ι : Type*} {X : ι → Type*} + [∀ i, MeasurableSpace (X i)] {μ : (i : ι) → Measure (X i)} {i : ι} + (h : ¬ IsProbabilityMeasure (μ i)) : + Measure.infinitePi μ = 0 := by + have h' : ¬ ∀ j, IsProbabilityMeasure (μ j) := fun h' ↦ h (h' i) + simp [Measure.infinitePi, h'] + open ProbabilityTheory Finset in /-- **The first terms of an i.i.d. sequence and the next terms are independent.** For an i.i.d. sequence `z` of law `μ`, the first `n` terms `(z i)_{i < n}` lie in `B` and the next `m` terms lie