From 099373d59455efa65d0b4b8efcfacbf889dfcb5f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:09:48 +0100 Subject: [PATCH 1/5] feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The value at time `n` of an e-process for the i.i.d. laws of a null, in the filtration of the observations, is a function of the first `n + 1` observations with expectation at most one under the null, hence an `n + 1`-sample e-variable composed with the initial segment. Its expected logarithm under the i.i.d. law of the alternative is at most `maxLogGrowth Q₁ S₁ (n + 1)`, and at most `(n + 1) * bipolarRate Q₁ S₁` (EValues roadmap, Layer 6.1). Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- LMLExplore/EValues/BipolarRate/EProcess.lean | 192 +++++++++++++++++++ 1 file changed, 192 insertions(+) create mode 100644 LMLExplore/EValues/BipolarRate/EProcess.lean diff --git a/LMLExplore/EValues/BipolarRate/EProcess.lean b/LMLExplore/EValues/BipolarRate/EProcess.lean new file mode 100644 index 00000000..b3f101dd --- /dev/null +++ b/LMLExplore/EValues/BipolarRate/EProcess.lean @@ -0,0 +1,192 @@ +/- +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 +public import LMLExplore.EValues.EProcess +public import Mathlib.MeasureTheory.Function.FactorsThrough +public import Mathlib.Probability.Independence.InfinitePi + +/-! +# E-processes for an i.i.d. null grow at most at the bipolar rate, in expectation + +Let `S₁` be a set of probability measures on `𝓧` (the null) and `Q₁` a probability measure on `𝓧` +(the alternative). The observations are the coordinates of `ℕ → 𝓧`, with the i.i.d. laws +`Measure.infinitePi fun _ ↦ P`, `P ∈ S₁`, and the filtration `Filtration.piLE`, whose σ-algebra at +time `n` is generated by the observations `0, …, n`. The value at time `n` of an e-process for the +i.i.d. null is a function of the first `n + 1` observations with expectation at most one under the +null, that is, an `n + 1`-sample e-variable. So its expected logarithm under the i.i.d. law of `Q₁` +is at most `maxLogGrowth Q₁ S₁ (n + 1)`, hence at most `(n + 1) * bipolarRate Q₁ S₁`: no e-process +grows faster than the bipolar rate, in expectation [RR26, Lemma 3.3]. + +## Main definitions + +* `ProbabilityTheory.initSeg n`: the first `n` observations of a sequence, as a function on + `Fin n`. + +## Main statements + +* `ProbabilityTheory.measurePreserving_initSeg`: the first `n` observations of an i.i.d. sequence + have the product law. +* `ProbabilityTheory.eintegral_log_le_maxLogGrowth_of_dependsOn`: a function of the first `n` + observations with expectation at most one under the i.i.d. laws of the null has expected + logarithm at most `maxLogGrowth Q₁ S₁ n` under the i.i.d. law of `Q₁`. +* `ProbabilityTheory.IsEProcess.eintegral_log_le_maxLogGrowth`, + `ProbabilityTheory.IsEProcess.eintegral_log_le_mul_bipolarRate`: the bound for the value of an + e-process at time `n`, by `maxLogGrowth Q₁ S₁ (n + 1)` and by `(n + 1) * bipolarRate Q₁ S₁`. +* `ProbabilityTheory.IsEProcess.eintegral_log_div_le_bipolarRate`, + `ProbabilityTheory.IsEProcess.limsup_eintegral_log_div_le_bipolarRate`: the expected logarithm + of an e-process at time `n`, divided by the number `n + 1` of observations it has seen, is at + most the bipolar rate, and so is its `limsup` [RR26, Lemma 3.3]. + +## References + +* [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1. +-/ + +public section + +open MeasureTheory Filter +open scoped ENNReal Topology + +namespace ProbabilityTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {Q₁ : Measure 𝓧} {S₁ : Set (Measure 𝓧)} + +/-! ### The first observations of a sequence -/ + +/-- The first `n` observations of a sequence. -/ +def initSeg (n : ℕ) (ω : ℕ → 𝓧) : Fin n → 𝓧 := fun i ↦ ω i + +/-- The coordinates of the initial segment are the first coordinates of the sequence. -/ +@[simp] +lemma initSeg_apply (n : ℕ) (ω : ℕ → 𝓧) (i : Fin n) : initSeg n ω i = ω i := (rfl) + +/-- The initial segment is a measurable function of the sequence. -/ +@[fun_prop] +lemma measurable_initSeg (n : ℕ) : Measurable (initSeg (𝓧 := 𝓧) n) := + Measurable.of_eval fun _ ↦ measurable_pi_apply _ + +/-- A measurable function of the first `n` observations is a measurable function of the initial +segment of length `n`. -/ +lemma exists_measurable_eq_comp_initSeg [Nonempty 𝓧] {β : Type*} [MeasurableSpace β] + {f : (ℕ → 𝓧) → β} {n : ℕ} (hf : Measurable f) (hfn : DependsOn f (Set.Iio n)) : + ∃ g : (Fin n → 𝓧) → β, Measurable g ∧ f = g ∘ initSeg n := by + classical + -- extend a finite sequence by a constant + let x₀ : 𝓧 := Classical.arbitrary 𝓧 + let ext : (Fin n → 𝓧) → ℕ → 𝓧 := fun y i ↦ if h : i < n then y ⟨i, h⟩ else x₀ + have hext : Measurable ext := by + refine Measurable.of_eval fun i ↦ ?_ + by_cases h : i < n + · simp only [ext, h, ↓reduceDIte] + exact measurable_pi_apply _ + · simp only [ext, h, ↓reduceDIte] + exact measurable_const + refine ⟨f ∘ ext, hf.comp hext, funext fun ω ↦ hfn fun i hi ↦ ?_⟩ + simp only [Set.mem_Iio] at hi + simp [ext, hi] + +/-- The first `n` observations of an i.i.d. sequence have the product law. -/ +lemma measurePreserving_initSeg (P : Measure 𝓧) [IsProbabilityMeasure P] (n : ℕ) : + MeasurePreserving (initSeg n) (Measure.infinitePi fun _ : ℕ ↦ P) + (Measure.pi fun _ : Fin n ↦ P) := by + refine ⟨measurable_initSeg n, ?_⟩ + rw [← Measure.infinitePi_eq_pi] + exact Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective + +/-! ### Functions of the first observations as e-variables of a sample -/ + +/-- A function of the first `n` observations with expectation at most one under the i.i.d. laws of +the members of `S₁` is an `n`-sample e-variable, composed with the initial segment. -/ +lemma exists_isEVar_eq_comp_initSeg [Nonempty 𝓧] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + {F : (ℕ → 𝓧) → ℝ≥0∞} {n : ℕ} (hF : Measurable F) (hFn : DependsOn F (Set.Iio n)) + (h_null : ∀ P ∈ S₁, ∫⁻ ω, F ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) : + ∃ G : (Fin n → 𝓧) → ℝ≥0∞, + IsEVar G ((fun P ↦ Measure.pi fun _ : Fin n ↦ P) '' S₁) ∧ F = G ∘ initSeg n := by + obtain ⟨G, hG, rfl⟩ := exists_measurable_eq_comp_initSeg hF hFn + refine ⟨G, IsEVar.of_lintegral_le_one ?_ hG ?_, rfl⟩ + · rintro _ ⟨P, hP, rfl⟩ + have := hS₁ P hP + infer_instance + · rintro _ ⟨P, hP, rfl⟩ + have := hS₁ P hP + rw [← (measurePreserving_initSeg P n).lintegral_comp hG] + exact h_null P hP + +/-- A function of the first `n` observations with expectation at most one under the i.i.d. laws of +the members of `S₁` has expected logarithm, under the i.i.d. law of `Q₁`, at most the maximal +expected logarithm of an `n`-sample e-variable. -/ +theorem eintegral_log_le_maxLogGrowth_of_dependsOn (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] + (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) {F : (ℕ → 𝓧) → ℝ≥0∞} {n : ℕ} (hF : Measurable F) + (hFn : DependsOn F (Set.Iio n)) + (h_null : ∀ P ∈ S₁, ∫⁻ ω, F ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) ≤ 1) : + ∫ᵉ ω, ENNReal.log (F ω) ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁) ≤ maxLogGrowth Q₁ S₁ n := by + have := nonempty_of_isProbabilityMeasure Q₁ + obtain ⟨G, hGe, rfl⟩ := exists_isEVar_eq_comp_initSeg hS₁ hF hFn h_null + calc ∫ᵉ ω, ENNReal.log ((G ∘ initSeg n) ω) ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁) + _ = ∫ᵉ x, (logUtility ∘ G) x ∂Measure.pi (fun _ : Fin n ↦ Q₁) := by + rw [← (measurePreserving_initSeg Q₁ n).map_eq, + eintegral_map (logUtility.measurable.comp hGe.measurable) (measurable_initSeg n)] + rfl + _ ≤ maxLogGrowth Q₁ S₁ n := by + rw [maxLogGrowth_def] + exact hGe.eintegral_le_maxUtility _ _ + +/-! ### E-processes -/ + +variable {E : ℕ → (ℕ → 𝓧) → ℝ≥0∞} + +/-- The value at time `n` of an e-process for the i.i.d. laws of the members of `S₁`, in the +filtration of the observations, has expected logarithm under the i.i.d. law of `Q₁` at most the +maximal expected logarithm of an `n + 1`-sample e-variable: at time `n` the process has seen +`n + 1` observations. -/ +theorem IsEProcess.eintegral_log_le_maxLogGrowth (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] + (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + (hE : IsEProcess E (Filtration.piLE (X := fun _ : ℕ ↦ 𝓧)) + ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁)) (n : ℕ) : + ∫ᵉ ω, ENNReal.log (E n ω) ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁) ≤ + maxLogGrowth Q₁ S₁ (n + 1) := by + refine eintegral_log_le_maxLogGrowth_of_dependsOn Q₁ hS₁ (hE.measurable n) ?_ fun P hP ↦ ?_ + · exact fun ω ω' h ↦ (hE.adapted n).dependsOn_of_piLE + fun i hi ↦ h i (Nat.lt_succ_of_le (Set.mem_Iic.1 hi)) + · have := hS₁ P hP + simpa using (hE.isEVar n).lintegral_le_measure_univ _ ⟨P, hP, rfl⟩ + +/-- The value at time `n` of an e-process for an i.i.d. null has expected logarithm, under the +i.i.d. law of `Q₁`, at most `n + 1` times the bipolar rate [RR26, Lemma 3.3]. -/ +theorem IsEProcess.eintegral_log_le_mul_bipolarRate (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] + (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + (hE : IsEProcess E (Filtration.piLE (X := fun _ : ℕ ↦ 𝓧)) + ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁)) (n : ℕ) : + ∫ᵉ ω, ENNReal.log (E n ω) ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁) ≤ + ((n + 1 : ℕ) : EReal) * bipolarRate Q₁ S₁ := + (hE.eintegral_log_le_maxLogGrowth Q₁ hS₁ n).trans + (maxLogGrowth_le_mul_bipolarRate Q₁ S₁ n.succ_ne_zero) + +/-- The expected logarithm of an e-process for an i.i.d. null at time `n`, per observation seen, is +at most the bipolar rate. -/ +theorem IsEProcess.eintegral_log_div_le_bipolarRate (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] + (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + (hE : IsEProcess E (Filtration.piLE (X := fun _ : ℕ ↦ 𝓧)) + ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁)) (n : ℕ) : + (∫ᵉ ω, ENNReal.log (E n ω) ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁)) / ((n + 1 : ℕ) : EReal) ≤ + bipolarRate Q₁ S₁ := + (EReal.div_le_iff_le_mul (by exact_mod_cast n.succ_pos) (EReal.natCast_ne_top _)).2 + (hE.eintegral_log_le_mul_bipolarRate Q₁ hS₁ n) + +/-- No e-process for an i.i.d. null grows faster than the bipolar rate, in expectation: the +expected logarithm at time `n` under the i.i.d. law of `Q₁`, divided by the number `n + 1` of +observations seen, has `limsup` at most the bipolar rate [RR26, Lemma 3.3]. -/ +theorem IsEProcess.limsup_eintegral_log_div_le_bipolarRate (Q₁ : Measure 𝓧) + [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + (hE : IsEProcess E (Filtration.piLE (X := fun _ : ℕ ↦ 𝓧)) + ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁)) : + limsup (fun n : ℕ ↦ (∫ᵉ ω, ENNReal.log (E n ω) ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁)) / + ((n + 1 : ℕ) : EReal)) atTop ≤ bipolarRate Q₁ S₁ := + limsup_le_iSup.trans (iSup_le fun n ↦ hE.eintegral_log_div_le_bipolarRate Q₁ hS₁ n) + +end ProbabilityTheory From beea8eda32f320f670ee3e4580d182a421ca1ddf Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:32:55 +0100 Subject: [PATCH 2/5] refactor: move initSeg API to the product-measure file Move initSeg, initSeg_apply, measurable_initSeg, exists_measurable_eq_comp_initSeg and measurePreserving_initSeg to LMLExplore/Probability/ProductMeasure.lean (namespace MeasureTheory), and close the logUtility step by logUtility_apply instead of rfl. Co-Authored-By: Claude Code --- LMLExplore/EValues/BipolarRate/EProcess.lean | 55 ++---------------- LMLExplore/Probability/ProductMeasure.lean | 59 +++++++++++++++++++- 2 files changed, 62 insertions(+), 52 deletions(-) diff --git a/LMLExplore/EValues/BipolarRate/EProcess.lean b/LMLExplore/EValues/BipolarRate/EProcess.lean index b3f101dd..8194c8be 100644 --- a/LMLExplore/EValues/BipolarRate/EProcess.lean +++ b/LMLExplore/EValues/BipolarRate/EProcess.lean @@ -7,8 +7,7 @@ module public import LMLExplore.EValues.BipolarRate public import LMLExplore.EValues.EProcess -public import Mathlib.MeasureTheory.Function.FactorsThrough -public import Mathlib.Probability.Independence.InfinitePi +public import LMLExplore.Probability.ProductMeasure /-! # E-processes for an i.i.d. null grow at most at the bipolar rate, in expectation @@ -22,15 +21,11 @@ null, that is, an `n + 1`-sample e-variable. So its expected logarithm under the is at most `maxLogGrowth Q₁ S₁ (n + 1)`, hence at most `(n + 1) * bipolarRate Q₁ S₁`: no e-process grows faster than the bipolar rate, in expectation [RR26, Lemma 3.3]. -## Main definitions - -* `ProbabilityTheory.initSeg n`: the first `n` observations of a sequence, as a function on - `Fin n`. +The first `n` observations are `MeasureTheory.initSeg n`, whose law under an i.i.d. sequence is the +product law (`MeasureTheory.measurePreserving_initSeg`). ## Main statements -* `ProbabilityTheory.measurePreserving_initSeg`: the first `n` observations of an i.i.d. sequence - have the product law. * `ProbabilityTheory.eintegral_log_le_maxLogGrowth_of_dependsOn`: a function of the first `n` observations with expectation at most one under the i.i.d. laws of the null has expected logarithm at most `maxLogGrowth Q₁ S₁ n` under the i.i.d. law of `Q₁`. @@ -56,48 +51,6 @@ namespace ProbabilityTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {Q₁ : Measure 𝓧} {S₁ : Set (Measure 𝓧)} -/-! ### The first observations of a sequence -/ - -/-- The first `n` observations of a sequence. -/ -def initSeg (n : ℕ) (ω : ℕ → 𝓧) : Fin n → 𝓧 := fun i ↦ ω i - -/-- The coordinates of the initial segment are the first coordinates of the sequence. -/ -@[simp] -lemma initSeg_apply (n : ℕ) (ω : ℕ → 𝓧) (i : Fin n) : initSeg n ω i = ω i := (rfl) - -/-- The initial segment is a measurable function of the sequence. -/ -@[fun_prop] -lemma measurable_initSeg (n : ℕ) : Measurable (initSeg (𝓧 := 𝓧) n) := - Measurable.of_eval fun _ ↦ measurable_pi_apply _ - -/-- A measurable function of the first `n` observations is a measurable function of the initial -segment of length `n`. -/ -lemma exists_measurable_eq_comp_initSeg [Nonempty 𝓧] {β : Type*} [MeasurableSpace β] - {f : (ℕ → 𝓧) → β} {n : ℕ} (hf : Measurable f) (hfn : DependsOn f (Set.Iio n)) : - ∃ g : (Fin n → 𝓧) → β, Measurable g ∧ f = g ∘ initSeg n := by - classical - -- extend a finite sequence by a constant - let x₀ : 𝓧 := Classical.arbitrary 𝓧 - let ext : (Fin n → 𝓧) → ℕ → 𝓧 := fun y i ↦ if h : i < n then y ⟨i, h⟩ else x₀ - have hext : Measurable ext := by - refine Measurable.of_eval fun i ↦ ?_ - by_cases h : i < n - · simp only [ext, h, ↓reduceDIte] - exact measurable_pi_apply _ - · simp only [ext, h, ↓reduceDIte] - exact measurable_const - refine ⟨f ∘ ext, hf.comp hext, funext fun ω ↦ hfn fun i hi ↦ ?_⟩ - simp only [Set.mem_Iio] at hi - simp [ext, hi] - -/-- The first `n` observations of an i.i.d. sequence have the product law. -/ -lemma measurePreserving_initSeg (P : Measure 𝓧) [IsProbabilityMeasure P] (n : ℕ) : - MeasurePreserving (initSeg n) (Measure.infinitePi fun _ : ℕ ↦ P) - (Measure.pi fun _ : Fin n ↦ P) := by - refine ⟨measurable_initSeg n, ?_⟩ - rw [← Measure.infinitePi_eq_pi] - exact Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective - /-! ### Functions of the first observations as e-variables of a sample -/ /-- A function of the first `n` observations with expectation at most one under the i.i.d. laws of @@ -131,7 +84,7 @@ theorem eintegral_log_le_maxLogGrowth_of_dependsOn (Q₁ : Measure 𝓧) [IsProb _ = ∫ᵉ x, (logUtility ∘ G) x ∂Measure.pi (fun _ : Fin n ↦ Q₁) := by rw [← (measurePreserving_initSeg Q₁ n).map_eq, eintegral_map (logUtility.measurable.comp hGe.measurable) (measurable_initSeg n)] - rfl + simp only [Function.comp_apply, logUtility_apply] _ ≤ maxLogGrowth Q₁ S₁ n := by rw [maxLogGrowth_def] exact hGe.eintegral_le_maxUtility _ _ diff --git a/LMLExplore/Probability/ProductMeasure.lean b/LMLExplore/Probability/ProductMeasure.lean index 21c9aec0..93314c21 100644 --- a/LMLExplore/Probability/ProductMeasure.lean +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -11,16 +11,73 @@ public import Mathlib.Probability.Independence.InfinitePi # 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 and the next `m` coordinates are independent. +`n` coordinates have the product law `Measure.pi`, and they are independent of the next `m` +coordinates. + +## Main definitions + +* `MeasureTheory.initSeg n`: the first `n` terms of a sequence, as a function on `Fin n`. ## Main statements +* `MeasureTheory.exists_measurable_eq_comp_initSeg`: a measurable function of the first `n` terms + of a sequence factors measurably through `initSeg n`. +* `MeasureTheory.measurePreserving_initSeg`: the first `n` terms of an i.i.d. sequence 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. -/ public section +namespace MeasureTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-! ### The first terms of a sequence -/ + +/-- The first `n` terms of a sequence. -/ +def initSeg (n : ℕ) (ω : ℕ → 𝓧) : Fin n → 𝓧 := fun i ↦ ω i + +/-- The coordinates of the initial segment are the first coordinates of the sequence. -/ +@[simp] +lemma initSeg_apply (n : ℕ) (ω : ℕ → 𝓧) (i : Fin n) : initSeg n ω i = ω i := (rfl) + +/-- The initial segment is a measurable function of the sequence. -/ +@[fun_prop] +lemma measurable_initSeg (n : ℕ) : Measurable (initSeg (𝓧 := 𝓧) n) := + Measurable.of_eval fun _ ↦ measurable_pi_apply _ + +/-- A measurable function of the first `n` terms of a sequence is a measurable function of the +initial segment of length `n`. -/ +lemma exists_measurable_eq_comp_initSeg [Nonempty 𝓧] {β : Type*} [MeasurableSpace β] + {f : (ℕ → 𝓧) → β} {n : ℕ} (hf : Measurable f) (hfn : DependsOn f (Set.Iio n)) : + ∃ g : (Fin n → 𝓧) → β, Measurable g ∧ f = g ∘ initSeg n := by + classical + -- extend a finite sequence by a constant + let x₀ : 𝓧 := Classical.arbitrary 𝓧 + let ext : (Fin n → 𝓧) → ℕ → 𝓧 := fun y i ↦ if h : i < n then y ⟨i, h⟩ else x₀ + have hext : Measurable ext := by + refine Measurable.of_eval fun i ↦ ?_ + by_cases h : i < n + · simp only [ext, h, ↓reduceDIte] + exact measurable_pi_apply _ + · simp only [ext, h, ↓reduceDIte] + exact measurable_const + refine ⟨f ∘ ext, hf.comp hext, funext fun ω ↦ hfn fun i hi ↦ ?_⟩ + simp only [Set.mem_Iio] at hi + simp [ext, hi] + +/-- The first `n` terms of an i.i.d. sequence have the product law. -/ +lemma measurePreserving_initSeg (P : Measure 𝓧) [IsProbabilityMeasure P] (n : ℕ) : + MeasurePreserving (initSeg n) (Measure.infinitePi fun _ : ℕ ↦ P) + (Measure.pi fun _ : Fin n ↦ P) := by + refine ⟨measurable_initSeg n, ?_⟩ + rw [← Measure.infinitePi_eq_pi] + exact Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective + +end MeasureTheory + namespace MeasureTheory.Measure open ProbabilityTheory Finset in From 1f1f4f901cacdbddb77fe7ed6daf5147b06782dd Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:58:26 +0100 Subject: [PATCH 3/5] Recover retained repair 5fac1fd677c84001828e090d9521a146 --- .../MeasurableSpace/Constructions.lean | 49 +++++++++++++++++ LMLExplore/Probability/ProductMeasure.lean | 53 +++---------------- .../SequentialLearning/StaticAllocation.lean | 2 +- 3 files changed, 57 insertions(+), 47 deletions(-) diff --git a/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean b/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean index 5f8958c7..f741686d 100644 --- a/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean +++ b/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean @@ -11,6 +11,10 @@ public import Mathlib.MeasureTheory.Group.Arithmetic /-! # Measurability of evaluations, initial segments of tuples and finite dependence +## Main definitions + +* `MeasureTheory.initSeg n`: the first `n` terms of a sequence, as a function on `Fin n`. + ## Main statements * `MeasureTheory.measurable_div_apply`: for a finite type `α` with measurable singletons and @@ -19,6 +23,8 @@ public import Mathlib.MeasureTheory.Group.Arithmetic evaluating row `i` of a table `x : ι → α → β` at `a : α` is measurable in the pair `(x, a)`. * `MeasureTheory.measurable_finInit`: the map `Fin.init` dropping the last entry of a tuple of length `n + 1` is measurable. +* `MeasureTheory.exists_measurable_eq_comp_initSeg`: a measurable function of the first `n` terms + of a sequence factors measurably through the initial segment `initSeg n`. * `DependsOn.measurable_of_countable`: a function of a family of countable variables with measurable singletons that only depends on finitely many of them is measurable. -/ @@ -69,4 +75,47 @@ lemma _root_.DependsOn.measurable_of_countable {ι : Type*} {X : ι → Type*} obtain ⟨g, rfl⟩ := dependsOn_iff_exists_comp.1 hf exact (_root_.measurable_of_countable g).comp (Measurable.of_eval fun i ↦ measurable_pi_apply _) +/-! ### The first terms of a sequence -/ + +section InitSeg + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-- The first `n` terms of a sequence. -/ +def initSeg (n : ℕ) (ω : ℕ → 𝓧) : Fin n → 𝓧 := fun i ↦ ω i + +/-- The initial segment of length `n` restricts a sequence to its first `n` indices. -/ +lemma initSeg_def (n : ℕ) : initSeg (𝓧 := 𝓧) n = fun ω i ↦ ω i := (rfl) + +/-- The coordinates of the initial segment are the first coordinates of the sequence. -/ +@[simp] +lemma initSeg_apply (n : ℕ) (ω : ℕ → 𝓧) (i : Fin n) : initSeg n ω i = ω i := (rfl) + +/-- The initial segment is a measurable function of the sequence. -/ +@[fun_prop] +lemma measurable_initSeg (n : ℕ) : Measurable (initSeg (𝓧 := 𝓧) n) := + Measurable.of_eval fun _ ↦ measurable_pi_apply _ + +/-- A measurable function of the first `n` terms of a sequence is a measurable function of the +initial segment of length `n`. -/ +lemma exists_measurable_eq_comp_initSeg [Nonempty 𝓧] {β : Type*} [MeasurableSpace β] + {f : (ℕ → 𝓧) → β} {n : ℕ} (hf : Measurable f) (hfn : DependsOn f (Set.Iio n)) : + ∃ g : (Fin n → 𝓧) → β, Measurable g ∧ f = g ∘ initSeg n := by + classical + -- extend a finite sequence by a constant + let x₀ : 𝓧 := Classical.arbitrary 𝓧 + let ext : (Fin n → 𝓧) → ℕ → 𝓧 := fun y i ↦ if h : i < n then y ⟨i, h⟩ else x₀ + have hext : Measurable ext := by + refine Measurable.of_eval fun i ↦ ?_ + by_cases h : i < n + · simp only [ext, h, ↓reduceDIte] + exact measurable_pi_apply _ + · simp only [ext, h, ↓reduceDIte] + exact measurable_const + refine ⟨f ∘ ext, hf.comp hext, funext fun ω ↦ hfn fun i hi ↦ ?_⟩ + simp only [Set.mem_Iio] at hi + simp [ext, hi] + +end InitSeg + end MeasureTheory diff --git a/LMLExplore/Probability/ProductMeasure.lean b/LMLExplore/Probability/ProductMeasure.lean index 93314c21..6a6c53cc 100644 --- a/LMLExplore/Probability/ProductMeasure.lean +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -5,6 +5,7 @@ Authors: LMLExplore contributors -/ module +public import LMLExplore.MeasureTheory.MeasurableSpace.Constructions public import Mathlib.Probability.Independence.InfinitePi /-! @@ -14,16 +15,10 @@ Under the infinite product `Measure.infinitePi` of copies of a probability measu `n` coordinates have the product law `Measure.pi`, and they are independent of the next `m` coordinates. -## Main definitions - -* `MeasureTheory.initSeg n`: the first `n` terms of a sequence, as a function on `Fin n`. - ## Main statements -* `MeasureTheory.exists_measurable_eq_comp_initSeg`: a measurable function of the first `n` terms - of a sequence factors measurably through `initSeg n`. -* `MeasureTheory.measurePreserving_initSeg`: the first `n` terms of an i.i.d. sequence have the - product law. +* `MeasureTheory.measurePreserving_initSeg`: the first `n` terms `initSeg n` of an i.i.d. sequence + 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. -/ @@ -34,46 +29,12 @@ namespace MeasureTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} -/-! ### The first terms of a sequence -/ - -/-- The first `n` terms of a sequence. -/ -def initSeg (n : ℕ) (ω : ℕ → 𝓧) : Fin n → 𝓧 := fun i ↦ ω i - -/-- The coordinates of the initial segment are the first coordinates of the sequence. -/ -@[simp] -lemma initSeg_apply (n : ℕ) (ω : ℕ → 𝓧) (i : Fin n) : initSeg n ω i = ω i := (rfl) - -/-- The initial segment is a measurable function of the sequence. -/ -@[fun_prop] -lemma measurable_initSeg (n : ℕ) : Measurable (initSeg (𝓧 := 𝓧) n) := - Measurable.of_eval fun _ ↦ measurable_pi_apply _ - -/-- A measurable function of the first `n` terms of a sequence is a measurable function of the -initial segment of length `n`. -/ -lemma exists_measurable_eq_comp_initSeg [Nonempty 𝓧] {β : Type*} [MeasurableSpace β] - {f : (ℕ → 𝓧) → β} {n : ℕ} (hf : Measurable f) (hfn : DependsOn f (Set.Iio n)) : - ∃ g : (Fin n → 𝓧) → β, Measurable g ∧ f = g ∘ initSeg n := by - classical - -- extend a finite sequence by a constant - let x₀ : 𝓧 := Classical.arbitrary 𝓧 - let ext : (Fin n → 𝓧) → ℕ → 𝓧 := fun y i ↦ if h : i < n then y ⟨i, h⟩ else x₀ - have hext : Measurable ext := by - refine Measurable.of_eval fun i ↦ ?_ - by_cases h : i < n - · simp only [ext, h, ↓reduceDIte] - exact measurable_pi_apply _ - · simp only [ext, h, ↓reduceDIte] - exact measurable_const - refine ⟨f ∘ ext, hf.comp hext, funext fun ω ↦ hfn fun i hi ↦ ?_⟩ - simp only [Set.mem_Iio] at hi - simp [ext, hi] - /-- The first `n` terms of an i.i.d. sequence have the product law. -/ lemma measurePreserving_initSeg (P : Measure 𝓧) [IsProbabilityMeasure P] (n : ℕ) : MeasurePreserving (initSeg n) (Measure.infinitePi fun _ : ℕ ↦ P) (Measure.pi fun _ : Fin n ↦ P) := by refine ⟨measurable_initSeg n, ?_⟩ - rw [← Measure.infinitePi_eq_pi] + rw [initSeg_def, ← Measure.infinitePi_eq_pi] exact Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective end MeasureTheory @@ -87,7 +48,7 @@ in `C` with probability `μ^⊗n(B) μ(C)^m`. -/ theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (n m : ℕ) {B : Set (Fin n → X)} {C : Set X} (hB : MeasurableSet B) (hC : MeasurableSet C) : - (Measure.infinitePi fun _ : ℕ ↦ μ) {z | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + (Measure.infinitePi fun _ : ℕ ↦ μ) {z | initSeg n z ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = Measure.pi (fun _ : Fin n ↦ μ) B * μ C ^ m := by -- The first `n` terms and the next `m` terms are independent. have h_ind := (iIndepFun_infinitePi (P := fun _ : ℕ ↦ μ) (X := fun _ ↦ id) @@ -96,11 +57,11 @@ theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] ( simp only [id] at h_ind have h_fin : Measurable fun (u : {i // i ∈ range n} → X) (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩ := by fun_prop - have h_set : {z : ℕ → X | (fun i : Fin n ↦ z i) ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = + have h_set : {z : ℕ → X | initSeg n z ∈ B ∧ ∀ j < m, z (n + j) ∈ C} = (fun z (i : range n) ↦ z i) ⁻¹' ((fun u (i : Fin n) ↦ u ⟨i, mem_range.2 i.2⟩) ⁻¹' B) ∩ (fun z (i : Ico n (n + m)) ↦ z i) ⁻¹' (Set.univ.pi fun _ ↦ C) := by ext z - simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, + simp only [initSeg_def, Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, Set.mem_univ, true_implies, Subtype.forall, mem_Ico] refine and_congr Iff.rfl ⟨fun h i hi ↦ ?_, fun h j hj ↦ h _ ⟨by omega, by omega⟩⟩ obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hi.1 diff --git a/LMLExplore/SequentialLearning/StaticAllocation.lean b/LMLExplore/SequentialLearning/StaticAllocation.lean index bea20a39..a9a1de5e 100644 --- a/LMLExplore/SequentialLearning/StaticAllocation.lean +++ b/LMLExplore/SequentialLearning/StaticAllocation.lean @@ -278,7 +278,7 @@ theorem exists_eventually_le_streamMeasure_forall_mean_mem Metric.isOpen_ball.measurableSet) Metric.isClosed_closedBall.measurableSet] congr 1 ext z - simp only [E, Set.mem_ofPred_eq, Set.mem_preimage, + simp only [E, Set.mem_ofPred_eq, Set.mem_preimage, initSeg_apply, Fin.sum_univ_eq_sum_range (fun i ↦ z i)] rw [streamMeasure_forall_arm_mem ν hE, Finset.prod_congr rfl fun a _ ↦ hE_eq a, Finset.prod_mul_distrib, mul_comm] From 6bd7863c01a5b13f4de1d0f40f4a1e3d861c5def Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 13:32:27 +0100 Subject: [PATCH 4/5] refactor: add dependsOn_initSeg and move BipolarRate to BipolarRate/Basic Add the introduction lemmas dependsOn_initSeg and dependsOn_comp_initSeg, converse to exists_measurable_eq_comp_initSeg, and move the module LMLExplore.EValues.BipolarRate to LMLExplore.EValues.BipolarRate.Basic next to the new BipolarRate/EProcess.lean. Co-Authored-By: Claude Code --- .../{BipolarRate.lean => BipolarRate/Basic.lean} | 0 LMLExplore/EValues/BipolarRate/EProcess.lean | 2 +- .../MeasurableSpace/Constructions.lean | 16 ++++++++++++++-- 3 files changed, 15 insertions(+), 3 deletions(-) rename LMLExplore/EValues/{BipolarRate.lean => BipolarRate/Basic.lean} (100%) diff --git a/LMLExplore/EValues/BipolarRate.lean b/LMLExplore/EValues/BipolarRate/Basic.lean similarity index 100% rename from LMLExplore/EValues/BipolarRate.lean rename to LMLExplore/EValues/BipolarRate/Basic.lean diff --git a/LMLExplore/EValues/BipolarRate/EProcess.lean b/LMLExplore/EValues/BipolarRate/EProcess.lean index 8194c8be..883ed395 100644 --- a/LMLExplore/EValues/BipolarRate/EProcess.lean +++ b/LMLExplore/EValues/BipolarRate/EProcess.lean @@ -5,7 +5,7 @@ Authors: LMLExplore contributors -/ module -public import LMLExplore.EValues.BipolarRate +public import LMLExplore.EValues.BipolarRate.Basic public import LMLExplore.EValues.EProcess public import LMLExplore.Probability.ProductMeasure diff --git a/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean b/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean index 5ff2434d..75cd8365 100644 --- a/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean +++ b/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean @@ -23,8 +23,10 @@ public import Mathlib.MeasureTheory.Group.Arithmetic evaluating row `i` of a table `x : ι → α → β` at `a : α` is measurable in the pair `(x, a)`. * `MeasureTheory.measurable_finInit`: the map `Fin.init` dropping the last entry of a tuple of length `n + 1` is measurable. -* `MeasureTheory.exists_measurable_eq_comp_initSeg`: a measurable function of the first `n` terms - of a sequence factors measurably through the initial segment `initSeg n`. +* `MeasureTheory.dependsOn_initSeg`, `MeasureTheory.dependsOn_comp_initSeg`: the initial segment + `initSeg n`, and any function of it, only depend on the first `n` terms of a sequence. +* `MeasureTheory.exists_measurable_eq_comp_initSeg`: conversely, a measurable function of the first + `n` terms of a sequence factors measurably through the initial segment `initSeg n`. * `DependsOn.measurable_of_countable`: a function of a family of countable variables with measurable singletons that only depends on finitely many of them is measurable. * `measurable_from_prod_of_dependsOn`: a function on a product whose first factor is a family of @@ -127,6 +129,16 @@ lemma initSeg_apply (n : ℕ) (ω : ℕ → 𝓧) (i : Fin n) : initSeg n ω i = lemma measurable_initSeg (n : ℕ) : Measurable (initSeg (𝓧 := 𝓧) n) := Measurable.of_eval fun _ ↦ measurable_pi_apply _ +/-- The initial segment of length `n` only depends on the first `n` terms of the sequence. -/ +lemma dependsOn_initSeg (n : ℕ) : DependsOn (initSeg (𝓧 := 𝓧) n) (Set.Iio n) := + fun _ _ h ↦ funext fun i ↦ h i i.isLt + +/-- A function of the initial segment of length `n` only depends on the first `n` terms of the +sequence. -/ +lemma dependsOn_comp_initSeg {β : Type*} {n : ℕ} (g : (Fin n → 𝓧) → β) : + DependsOn (g ∘ initSeg n) (Set.Iio n) := + fun _ _ h ↦ congrArg g (dependsOn_initSeg n h) + /-- A measurable function of the first `n` terms of a sequence is a measurable function of the initial segment of length `n`. -/ lemma exists_measurable_eq_comp_initSeg [Nonempty 𝓧] {β : Type*} [MeasurableSpace β] From cebeea2b1bb6aedc2922c48a5d5c3cd0f20aaeb8 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:16:21 +0100 Subject: [PATCH 5/5] refactor: reuse measurePreserving_initSeg for the first terms of an i.i.d. sequence Replace the inline re-derivations in infinitePi_fin_mem_and_forall_add_mem and hasLaw_arm_fin_streamMeasure by measurePreserving_initSeg. Co-Authored-By: Claude Code --- LMLExplore/Probability/ProductMeasure.lean | 6 ++---- LMLExplore/SequentialLearning/SumRewards.lean | 7 +++---- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/LMLExplore/Probability/ProductMeasure.lean b/LMLExplore/Probability/ProductMeasure.lean index 6a6c53cc..c218f9e8 100644 --- a/LMLExplore/Probability/ProductMeasure.lean +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -69,10 +69,8 @@ theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] ( rw [h_set, h_ind.measure_inter_preimage_eq_mul _ _ (h_fin hB) (.univ_pi fun _ ↦ hC)] congr 1 · -- The first `n` terms are `n` independent samples of `μ`. - have h_pi : (Measure.infinitePi fun _ : ℕ ↦ μ).map (fun z (i : Fin n) ↦ z i) = - Measure.pi fun _ : Fin n ↦ μ := by - rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi] - rw [← h_pi, Measure.map_apply (by fun_prop) hB, ← Set.preimage_comp] + rw [← (measurePreserving_initSeg μ n).map_eq, Measure.map_apply (measurable_initSeg n) hB, + ← Set.preimage_comp, initSeg_def] -- Both sides are the preimage of `B` under `z ↦ (z i)_{i : Fin n}`: the composite -- `(fun u i ↦ u ⟨i, _⟩) ∘ (fun z i ↦ z i)` unfolds to `fun z i ↦ z ↑⟨i, _⟩`, and -- `↑⟨i, _⟩ = i` is `Subtype.val` applied to a constructor. diff --git a/LMLExplore/SequentialLearning/SumRewards.lean b/LMLExplore/SequentialLearning/SumRewards.lean index a952bf4f..8b8f0b1b 100644 --- a/LMLExplore/SequentialLearning/SumRewards.lean +++ b/LMLExplore/SequentialLearning/SumRewards.lean @@ -8,6 +8,7 @@ module public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure public import LMLExplore.MeasureTheory.Integral.Lebesgue.Add public import LMLExplore.MeasureTheory.Measure.Prod +public import LMLExplore.Probability.ProductMeasure public import LMLExplore.SequentialLearning.FiniteActions public import Mathlib.Probability.StrongLaw @@ -356,10 +357,8 @@ theorem hasLaw_arm_fin_streamMeasure {𝓡 : Type*} [MeasurableSpace 𝓡] (ν : HasLaw (fun (ω : ℕ → α → 𝓡) (i : Fin n) ↦ ω i a) (Measure.pi fun _ : Fin n ↦ ν a) (streamMeasure ν) := by -- the first `n` terms of an i.i.d. sequence are `n` independent samples - have h_fin : HasLaw (fun (z : ℕ → 𝓡) (i : Fin n) ↦ z i) (Measure.pi fun _ : Fin n ↦ ν a) - (Measure.infinitePi fun _ : ℕ ↦ ν a) := - ⟨(Measurable.of_eval fun i : Fin n ↦ measurable_pi_apply (i : ℕ)).aemeasurable, by - rw [Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective, Measure.infinitePi_eq_pi]⟩ + have h_fin := (measurePreserving_initSeg (ν a) n).hasLaw + rw [initSeg_def] at h_fin exact h_fin.comp ((hasLaw_eval_infinitePi _ a).comp (hasLaw_arm_streamMeasure ν)) omit [DecidableEq α] [Countable α] [MeasurableSingletonClass α] in