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 new file mode 100644 index 00000000..883ed395 --- /dev/null +++ b/LMLExplore/EValues/BipolarRate/EProcess.lean @@ -0,0 +1,145 @@ +/- +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.Basic +public import LMLExplore.EValues.EProcess +public import LMLExplore.Probability.ProductMeasure + +/-! +# 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]. + +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.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 𝓧)} + +/-! ### 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)] + simp only [Function.comp_apply, logUtility_apply] + _ ≤ 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 diff --git a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean index a0218f90..cb1be17a 100644 --- a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean +++ b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean @@ -5,7 +5,7 @@ Authors: LMLExplore contributors -/ module -public import LMLExplore.EValues.BipolarRate +public import LMLExplore.EValues.BipolarRate.Basic public import LMLExplore.Probability.LargeDeviations.EmpiricalAverage /-! diff --git a/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean b/LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean index 1432e707..75cd8365 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,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.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 @@ -100,4 +108,57 @@ lemma _root_.measurable_from_prod_of_dependsOn {ι : Type*} {X : ι → Type*} ((measurable_pi_iff.2 fun i ↦ (measurable_pi_apply _).comp measurable_fst).prodMk measurable_snd) +/-! ### 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 _ + +/-- 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 β] + {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 21c9aec0..c218f9e8 100644 --- a/LMLExplore/Probability/ProductMeasure.lean +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -5,22 +5,40 @@ Authors: LMLExplore contributors -/ module +public import LMLExplore.MeasureTheory.MeasurableSpace.Constructions 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 statements +* `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. -/ public section +namespace MeasureTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-- 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 [initSeg_def, ← Measure.infinitePi_eq_pi] + exact Measure.map_infinitePi_infinitePi_of_inj Fin.val_injective + +end MeasureTheory + namespace MeasureTheory.Measure open ProbabilityTheory Finset in @@ -30,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) @@ -39,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 @@ -51,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/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] 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