Law of rewardByCount

LeanMachineLearning.lean

@@ -6,7 +6,9 @@ public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
 public import LeanMachineLearning.ForMathlib.MeasureTheory.OuterMeasure.Basic
 public import LeanMachineLearning.ForMathlib.Order.Interval.Finset
+public import LeanMachineLearning.ForMathlib.Probability.ConditionalProbability
 public import LeanMachineLearning.ForMathlib.Probability.HasCondDistrib
+public import LeanMachineLearning.ForMathlib.Probability.HasLaw
 public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib
 public import LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepFun
 public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun

LeanMachineLearning/ForMathlib/Probability/ConditionalProbability.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.Prod
+public import Mathlib.Probability.ConditionalProbability
+
+/-! # Lemmas about conditional probability
+-/
+
+@[expose] public section
+
+open MeasureTheory
+
+namespace ProbabilityTheory
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+
+/-- Conditioning a product measure on an event of the first coordinate amounts to conditioning
+the first measure. -/
+lemma cond_prod_univ {μ : Measure α} [SFinite μ] {ν : Measure β} [IsProbabilityMeasure ν]
+    (s : Set α) :
+    (μ.prod ν)[|s ×ˢ Set.univ] = (μ[|s]).prod ν := by
+  simp only [cond, Measure.prod_prod, measure_univ, mul_one, Measure.prod_smul_left,
+    ← Measure.prod_restrict, Measure.restrict_univ]
+
+end ProbabilityTheory

LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean

@@ -168,6 +168,63 @@ lemma ae_eq_of_hasCondDistrib_deterministic [MeasurableEq Ω] [SFinite μ] {f :
     AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
   rfl
 
+section Cond
+
+variable [IsSFiniteKernel κ]
+
+/-- If the conditional distribution of `Y` given `X` is a kernel `κ` which is constant equal to `η`
+on a measurable set `s`, then `μ (X ⁻¹' s ∩ Y ⁻¹' u) = μ (X ⁻¹' s) * η u` for all measurable `u`. -/
+lemma HasCondDistrib.measure_inter_preimage_eq_mul_of_eqOn_const [SFinite μ]
+    (h : HasCondDistrib Y X κ μ) {s : Set β} (hs : MeasurableSet s) {η : Measure Ω}
+    (hκ : Set.EqOn κ (fun _ ↦ η) s) {u : Set Ω} (hu : MeasurableSet u) :
+    μ (X ⁻¹' s ∩ Y ⁻¹' u) = μ (X ⁻¹' s) * η u := by
+  have h_eq : X ⁻¹' s ∩ Y ⁻¹' u = (fun ω ↦ (X ω, Y ω)) ⁻¹' (s ×ˢ u) := by
+    ext ω
+    simp
+  rw [h_eq, ← Measure.map_apply_of_aemeasurable h.aemeasurable (hs.prod hu), h.map_eq,
+    Measure.compProd_apply_prod hs hu,
+    setLIntegral_congr_fun hs (g := fun _ ↦ η u) (fun x hx ↦ by rw [hκ hx]),
+    setLIntegral_const, Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, mul_comm]
+
+variable [IsFiniteMeasure μ]
+
+/-- If the conditional distribution of `Y` given `X` is a kernel `κ` which is constant equal to `η`
+on a measurable set `s`, then the law of `Y` under `μ` conditioned on `X ∈ s` is `η`. -/
+lemma HasCondDistrib.hasLaw_cond (h : HasCondDistrib Y X κ μ) (hY : Measurable Y)
+    {s : Set β} (hs : MeasurableSet s) {η : Measure Ω} (hκ : Set.EqOn κ (fun _ ↦ η) s)
+    (hμs : μ (X ⁻¹' s) ≠ 0) :
+    HasLaw Y η μ[|X ⁻¹' s] where
+  aemeasurable := hY.aemeasurable
+  map_eq := by
+    ext u hu
+    rw [Measure.map_apply hY hu, cond_apply' (hu.preimage hY),
+      h.measure_inter_preimage_eq_mul_of_eqOn_const hs hκ hu, ← mul_assoc,
+      ENNReal.inv_mul_cancel hμs (measure_ne_top _ _), one_mul]
+
+/-- If the conditional distribution of `Y` given `X` is a kernel `κ` which is constant on a
+measurable set `s`, then `X` and `Y` are independent under `μ` conditioned on `X ∈ s`. -/
+lemma HasCondDistrib.indepFun_cond (h : HasCondDistrib Y X κ μ) (hX : Measurable X)
+    {s : Set β} (hs : MeasurableSet s) {η : Measure Ω} (hκ : Set.EqOn κ (fun _ ↦ η) s) :
+    X ⟂ᵢ[μ[|X ⁻¹' s]] Y := by
+  by_cases hμs : μ (X ⁻¹' s) = 0
+  · rw [cond_eq_zero.2 (Or.inr hμs)]
+    simp [indepFun_iff_measure_inter_preimage_eq_mul]
+  rw [indepFun_iff_measure_inter_preimage_eq_mul]
+  intro t u ht hu
+  have h1 : X ⁻¹' s ∩ (X ⁻¹' t ∩ Y ⁻¹' u) = X ⁻¹' (s ∩ t) ∩ Y ⁻¹' u := by
+    ext ω
+    simp only [Set.mem_inter_iff, Set.mem_preimage]
+    tauto
+  rw [cond_apply (hs.preimage hX), cond_apply (hs.preimage hX), cond_apply (hs.preimage hX), h1,
+    ← Set.preimage_inter,
+    h.measure_inter_preimage_eq_mul_of_eqOn_const (hs.inter ht) (hκ.mono Set.inter_subset_left)
+      hu,
+    h.measure_inter_preimage_eq_mul_of_eqOn_const hs hκ hu,
+    ← mul_assoc (μ (X ⁻¹' s))⁻¹ (μ (X ⁻¹' s)) (η u),
+    ENNReal.inv_mul_cancel hμs (measure_ne_top _ _), one_mul, mul_assoc]
+
+end Cond
+
 variable [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace Ω'] [Nonempty Ω']
 
 lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]

LeanMachineLearning/ForMathlib/Probability/HasLaw.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Constructions.Cylinders
+public import Mathlib.MeasureTheory.Integral.Indicator
+public import Mathlib.Probability.ConditionalProbability
+public import Mathlib.Probability.HasLaw
+public import Mathlib.Probability.IdentDistrib
+
+/-! # Lemmas about `HasLaw`
+-/
+
+@[expose] public section
+
+open MeasureTheory Filter
+open scoped Topology
+
+namespace ProbabilityTheory
+
+variable {Ω 𝓧 : Type*} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {P : Measure Ω}
+
+lemma _root_.AEMeasurable.hasLaw_map {X : Ω → 𝓧} (hX : AEMeasurable X P) :
+    HasLaw X (P.map X) P := ⟨hX, rfl⟩
+
+lemma _root_.Measurable.hasLaw_map {X : Ω → 𝓧} (hX : Measurable X) (P : Measure Ω) :
+    HasLaw X (P.map X) P := ⟨hX.aemeasurable, rfl⟩
+
+section Cond
+
+variable {ι : Type*} [Countable ι] {mι : MeasurableSpace ι} [MeasurableSingletonClass ι]
+
+/-- Two random variables which are identically distributed conditionally on each atom of a
+countable measurable partition are identically distributed. -/
+lemma identDistrib_of_forall_identDistrib_cond [IsFiniteMeasure P] {g : Ω → ι}
+    (hg : Measurable g) {X Y : Ω → 𝓧} (hX : Measurable X) (hY : Measurable Y)
+    (h : ∀ i, IdentDistrib X Y P[|g ⁻¹' {i}] P[|g ⁻¹' {i}]) :
+    IdentDistrib X Y P P where
+  aemeasurable_fst := hX.aemeasurable
+  aemeasurable_snd := hY.aemeasurable
+  map_eq := by
+    ext s hs
+    rw [Measure.map_apply hX hs, Measure.map_apply hY hs]
+    have h_union (t : Set Ω) : t = ⋃ i, t ∩ g ⁻¹' {i} := by ext; simp
+    have h_disj (t : Set Ω) : Pairwise (Function.onFun Disjoint fun i ↦ t ∩ g ⁻¹' {i}) := by
+      intro i j hij
+      rw [Function.onFun, Set.disjoint_left]
+      rintro x ⟨-, hi⟩ ⟨-, hj⟩
+      exact hij ((show g x = i from hi).symm.trans hj)
+    rw [h_union (X ⁻¹' s), h_union (Y ⁻¹' s),
+      measure_iUnion (h_disj _) fun i ↦ (hs.preimage hX).inter (hg (measurableSet_singleton i)),
+      measure_iUnion (h_disj _) fun i ↦ (hs.preimage hY).inter (hg (measurableSet_singleton i))]
+    refine tsum_congr fun i ↦ ?_
+    rw [Set.inter_comm, ← cond_mul_eq_inter (hg (measurableSet_singleton i)),
+      Set.inter_comm _ (g ⁻¹' {i}), ← cond_mul_eq_inter (hg (measurableSet_singleton i)),
+      ← Measure.map_apply hX hs, ← Measure.map_apply hY hs, (h i).map_eq]
+
+/-- If a random variable has law `μ` conditionally on each atom of positive probability of a
+countable measurable partition, then it has law `μ`. -/
+lemma hasLaw_of_forall_hasLaw_cond [IsProbabilityMeasure P] {g : Ω → ι} (hg : Measurable g)
+    {X : Ω → 𝓧} (hX : Measurable X) {μ : Measure 𝓧}
+    (h : ∀ i, P (g ⁻¹' {i}) ≠ 0 → HasLaw X μ P[|g ⁻¹' {i}]) :
+    HasLaw X μ P where
+  aemeasurable := hX.aemeasurable
+  map_eq := by
+    ext s hs
+    rw [Measure.map_apply hX hs]
+    have h_union : X ⁻¹' s = ⋃ i, X ⁻¹' s ∩ g ⁻¹' {i} := by ext; simp
+    have h_disj : Pairwise (Function.onFun Disjoint fun i ↦ X ⁻¹' s ∩ g ⁻¹' {i}) := by
+      intro i j hij
+      rw [Function.onFun, Set.disjoint_left]
+      rintro x ⟨-, hi⟩ ⟨-, hj⟩
+      exact hij ((show g x = i from hi).symm.trans hj)
+    have h_univ : Set.univ = ⋃ i, g ⁻¹' {i} := by ext; simp
+    have h_disj_univ : Pairwise (Function.onFun Disjoint fun i ↦ g ⁻¹' {i}) := by
+      intro i j hij
+      rw [Function.onFun, Set.disjoint_left]
+      exact fun x hi hj ↦ hij ((show g x = i from hi).symm.trans hj)
+    calc P (X ⁻¹' s)
+    _ = ∑' i, P (X ⁻¹' s ∩ g ⁻¹' {i}) := by
+      conv_lhs => rw [h_union]
+      exact measure_iUnion h_disj fun i ↦ (hs.preimage hX).inter (hg (measurableSet_singleton i))
+    _ = ∑' i, μ s * P (g ⁻¹' {i}) := by
+      refine tsum_congr fun i ↦ ?_
+      rw [Set.inter_comm, ← cond_mul_eq_inter (hg (measurableSet_singleton i))]
+      by_cases hi : P (g ⁻¹' {i}) = 0
+      · simp [hi]
+      · rw [← Measure.map_apply hX hs, (h i hi).map_eq]
+    _ = μ s := by
+      rw [ENNReal.tsum_mul_left, ← measure_iUnion h_disj_univ
+        fun i ↦ hg (measurableSet_singleton i), ← h_univ, measure_univ, mul_one]
+
+end Cond
+
+section Pi
+
+variable {ι : Type*} {𝓧 : ι → Type*} [∀ i, MeasurableSpace (𝓧 i)]
+
+/-- Let `Y n : Ω → Π i, 𝓧 i` be random variables with law `μ`, indexed by a countably generated
+filter `L`. If for every `ω` and `i`, `Y n ω i` is eventually equal to `Y' ω i` along `L`, then `Y'`
+also has law `μ`. -/
+lemma hasLaw_of_forall_eventually_eq [IsFiniteMeasure P] {κ : Type*} {L : Filter κ} [L.NeBot]
+    [L.IsCountablyGenerated] {μ : Measure (Π i, 𝓧 i)} {Y : κ → Ω → Π i, 𝓧 i} {Y' : Ω → Π i, 𝓧 i}
+    (hY : ∀ n, Measurable (Y n)) (hY' : AEMeasurable Y' P)
+    (h_law : ∀ n, HasLaw (Y n) μ P) (h_lim : ∀ ω i, ∀ᶠ n in L, Y n ω i = Y' ω i) :
+    HasLaw Y' μ P where
+  aemeasurable := hY'
+  map_eq := by
+    refine ext_of_generate_finite (measurableCylinders _) generateFrom_measurableCylinders.symm
+      isPiSystem_measurableCylinders (fun s hs ↦ ?_) ?_
+    · obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders s).1 hs
+      rw [Measure.map_apply_of_aemeasurable hY' (hS.cylinder _)]
+      have h_tendsto : Tendsto (fun n ↦ P (Y n ⁻¹' cylinder I S)) L
+          (𝓝 (P (Y' ⁻¹' cylinder I S))) := by
+        refine tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure L P
+          (fun n ↦ (hS.cylinder _).preimage (hY n)) fun ω ↦ ?_
+        have h_ev : ∀ᶠ n in L, ∀ i ∈ I, Y n ω i = Y' ω i :=
+          (eventually_all_finset I).2 fun i _ ↦ h_lim ω i
+        filter_upwards [h_ev] with n hn
+        simp only [Set.mem_preimage, mem_cylinder]
+        have : I.restrict (Y n ω) = I.restrict (Y' ω) := funext fun i ↦ hn i i.2
+        rw [this]
+      have h_const : Tendsto (fun n ↦ P (Y n ⁻¹' cylinder I S)) L (𝓝 (μ (cylinder I S))) := by
+        have : (fun n ↦ P (Y n ⁻¹' cylinder I S)) = fun _ ↦ μ (cylinder I S) := by
+          funext n
+          rw [← Measure.map_apply (hY n) (hS.cylinder _), (h_law n).map_eq]
+        rw [this]
+        exact tendsto_const_nhds
+      exact tendsto_nhds_unique h_tendsto h_const
+    · obtain ⟨n⟩ := L.nonempty_of_neBot
+      rw [Measure.map_apply_of_aemeasurable hY' MeasurableSet.univ, Set.preimage_univ,
+        ← (h_law n).map_eq,
+        Measure.map_apply (hY n) MeasurableSet.univ, Set.preimage_univ]
+
+end Pi
+
+end ProbabilityTheory

LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean

@@ -59,6 +59,24 @@ lemma indepFun_cond_comp {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ :
   simp_rw [h_preim]
   exact indepFun_cond_of_indepFun hXY hY (hZ (measurableSet_singleton z))
 
+/-- Under `μ` conditioned on the event `X = b`, the random variable `X` is almost surely constant,
+hence independent of any other random variable. -/
+lemma indepFun_cond_preimage_singleton_left {α β γ : Type*} {mα : MeasurableSpace α}
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSingletonClass β] {μ : Measure α}
+    {X : α → β} (hX : Measurable X) (b : β) (Y : α → γ) :
+    X ⟂ᵢ[μ[|X ⁻¹' {b}]] Y :=
+  (indepFun_const_left b Y).congr
+    (ae_cond_of_forall_mem (hX (measurableSet_singleton b)) fun x hx ↦ (hx : X x = b).symm)
+    Filter.EventuallyEq.rfl
+
+/-- Under `μ` conditioned on the event `X = b`, the random variable `X` is almost surely constant,
+hence independent of any other random variable. -/
+lemma indepFun_cond_preimage_singleton_right {α β γ : Type*} {mα : MeasurableSpace α}
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSingletonClass β] {μ : Measure α}
+    {X : α → β} (hX : Measurable X) (b : β) (Y : α → γ) :
+    Y ⟂ᵢ[μ[|X ⁻¹' {b}]] X :=
+  (indepFun_cond_preimage_singleton_left hX b Y).symm
+
 lemma iIndepFun_nat_iff_forall_indepFun [IsProbabilityMeasure μ] {X : ℕ → Ω → E}
     (hX : ∀ n, AEMeasurable (X n) μ) :
     iIndepFun X μ ↔ ∀ n, X (n + 1) ⟂ᵢ[μ] fun ω (i : Iic n) ↦ X i ω := by

LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

@@ -66,6 +66,13 @@ lemma hasLaw_eval_eval_streamMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν]
     HasLaw (fun h : ℕ → 𝓐 → 𝓡 ↦ h n a) (ν a) (streamMeasure ν) :=
   (hasLaw_eval_infinitePi ν a).comp (hasLaw_eval_streamMeasure ν n)
 
+/-- Under a product measure `μ.prod (streamMeasure ν)`, the entry `(n, a)` of the reward array has
+law `ν a`. -/
+lemma hasLaw_snd_apply_prod_streamMeasure {Ω : Type*} {mΩ : MeasurableSpace Ω} (μ : Measure Ω)
+    [IsProbabilityMeasure μ] (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) :
+    HasLaw (fun ω : Ω × (ℕ → 𝓐 → 𝓡) ↦ ω.2 n a) (ν a) (μ.prod (streamMeasure ν)) :=
+  (hasLaw_eval_eval_streamMeasure ν n a).comp (hasLaw_snd_prod μ _)
+
 lemma identDistrib_eval_eval_id_streamMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) :
     IdentDistrib (fun h : ℕ → 𝓐 → 𝓡 ↦ h n a) id (streamMeasure ν) (ν a) where
   aemeasurable_fst := Measurable.aemeasurable (by fun_prop)
@@ -107,6 +114,57 @@ lemma indepFun_eval_streamMeasure' (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] {
     IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (streamMeasure ν) :=
   indepFun_proj_infinitePi_infinitePi h
 
+/-- Under a product measure `μ.prod (streamMeasure ν)`, the entries of the reward array are
+independent. -/
+lemma iIndepFun_snd_apply_prod_streamMeasure {Ω : Type*} {mΩ : MeasurableSpace Ω} (μ : Measure Ω)
+    [IsProbabilityMeasure μ] (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] :
+    iIndepFun (fun (p : ℕ × 𝓐) (ω : Ω × (ℕ → 𝓐 → 𝓡)) ↦ ω.2 p.1 p.2)
+      (μ.prod (streamMeasure ν)) := by
+  have h_snd : (μ.prod (streamMeasure ν)).map Prod.snd = streamMeasure ν := Measure.snd_prod
+  rw [iIndepFun_iff_map_fun_eq_infinitePi_map (fun _ ↦ by fun_prop)]
+  calc (μ.prod (streamMeasure ν)).map (fun ω (i : ℕ × 𝓐) ↦ ω.2 i.1 i.2)
+  _ = ((μ.prod (streamMeasure ν)).map Prod.snd).map (fun z (i : ℕ × 𝓐) ↦ z i.1 i.2) := by
+    rw [Measure.map_map (by fun_prop) measurable_snd]
+    rfl
+  _ = Measure.infinitePi fun i : ℕ × 𝓐 ↦ (streamMeasure ν).map (fun z ↦ z i.1 i.2) := by
+    rw [h_snd]
+    exact (iIndepFun_iff_map_fun_eq_infinitePi_map (fun _ ↦ by fun_prop)).1
+      (iIndepFun_eval_streamMeasure ν)
+  _ = Measure.infinitePi fun i : ℕ × 𝓐 ↦
+      (μ.prod (streamMeasure ν)).map (fun ω ↦ ω.2 i.1 i.2) := by
+    refine congrArg _ (funext fun i ↦ ?_)
+    conv_lhs => rw [← h_snd]
+    rw [Measure.map_map (by fun_prop) measurable_snd]
+    rfl
+
+/-- Under a product measure `μ.prod (streamMeasure ν)`, the entry `(m, a)` of the reward array is
+independent of the pair formed by the first coordinate and the reward array in which the entry
+`(m, a)` is replaced by a constant `x`. -/
+lemma indepFun_snd_apply_prod_streamMeasure_update [DecidableEq 𝓐] {Ω : Type*}
+    {mΩ : MeasurableSpace Ω} (μ : Measure Ω) [IsProbabilityMeasure μ] (ν : Kernel 𝓐 𝓡)
+    [IsMarkovKernel ν] (m : ℕ) (a : 𝓐) (x : 𝓡) :
+    (fun ω : Ω × (ℕ → 𝓐 → 𝓡) ↦ ω.2 m a) ⟂ᵢ[μ.prod (streamMeasure ν)]
+      (fun ω ↦ (ω.1, fun i b ↦ if i = m ∧ b = a then x else ω.2 i b)) := by
+  let T : (ℕ → 𝓐 → 𝓡) → (ℕ → 𝓐 → 𝓡) := fun z i b ↦ if i = m ∧ b = a then x else z i b
+  have hT : Measurable[⨆ p ∈ {p : ℕ × 𝓐 | p ≠ (m, a)},
+      MeasurableSpace.comap (fun z : ℕ → 𝓐 → 𝓡 ↦ z p.1 p.2) inferInstance] T := by
+    rw [measurable_iff_comap_le, MeasurableSpace.comap_pi]
+    refine iSup_le fun i ↦ ?_
+    rw [MeasurableSpace.comap_pi]
+    refine iSup_le fun b ↦ ?_
+    by_cases hib : i = m ∧ b = a
+    · obtain ⟨rfl, rfl⟩ := hib
+      simp only [T, and_self, ↓reduceIte, MeasurableSpace.comap_const]
+      exact bot_le
+    · simp only [T, hib, ↓reduceIte]
+      refine le_iSup₂_of_le (i, b) ?_ le_rfl
+      simpa only [Set.mem_ofPred_eq, ne_eq, Prod.mk.injEq] using hib
+  have hTm : Measurable T :=
+    hT.mono (iSup₂_le fun p _ ↦ Measurable.comap_le (by fun_prop)) le_rfl
+  have h := (iIndepFun_eval_streamMeasure ν).indepFun_of_measurable_iSup_comap
+    (fun _ ↦ by fun_prop) (i := (m, a)) (by simp) hT
+  exact h.snd_prod (μ := μ) (by fun_prop) hTm
+
 end StreamMeasure
 
 namespace ArrayModel
@@ -133,7 +191,7 @@ lemma hasLaw_fst_apply_arrayMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν]
 
 lemma hasLaw_snd_apply_arrayMeasure (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) :
     HasLaw (fun ω : probSpace 𝓐 𝓡 ↦ ω.2 n a) (ν a) (arrayMeasure ν) :=
-  (hasLaw_eval_eval_streamMeasure ν n a).comp (hasLaw_snd_prod _ _)
+  hasLaw_snd_apply_prod_streamMeasure _ ν n a
 
 lemma map_snd_apply_arrayMeasure {ν : Kernel 𝓐 𝓡} [IsMarkovKernel ν] (n : ℕ) (a : 𝓐) :
     (arrayMeasure ν).map (fun ω ↦ ω.2 n a) = ν a :=