feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3]

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

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
 
 /-!

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

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,22 +57,20 @@ 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
     exact h j (by omega)
   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.

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]

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