Use upstreamed HasCondDistrib definition

LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean

@@ -6,7 +6,7 @@ Authors: Rémy Degenne, Paulo Rauber
 module
 
 public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib
-public import Mathlib.Probability.HasLaw
+public import Mathlib.Probability.HasCondDistrib
 
 /-!
 # A predicate for having a specified conditional distribution
@@ -20,98 +20,34 @@ namespace ProbabilityTheory
 
 variable {α β γ Ω Ω' : Type*}
   {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
-  {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω]
-  {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace Ω'] [Nonempty Ω']
+  {mΩ : MeasurableSpace Ω}
+  {mΩ' : MeasurableSpace Ω'}
   {μ : Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
 
-/-- Predicate stating that the conditional distribution of `Y` given `X` under the measure `μ`
-is equal to the kernel `κ`. -/
-structure HasCondDistrib (Y : α → Ω) (X : α → β) (κ : Kernel β Ω)
-  (μ : Measure α) [IsFiniteMeasure μ] : Prop where
-  aemeasurable_fst : AEMeasurable Y μ := by fun_prop
-  aemeasurable_snd : AEMeasurable X μ := by fun_prop
-  condDistrib_eq : condDistrib Y X μ =ᵐ[μ.map X] κ
-
-attribute [fun_prop] HasCondDistrib.aemeasurable_fst HasCondDistrib.aemeasurable_snd
-
-lemma hasCondDistrib_fst_prod {Y : α → Ω} {X : α → β}
-    {κ : Kernel β Ω}
+lemma hasCondDistrib_fst_prod {Y : α → Ω} {X : α → β} {κ : Kernel β Ω}
     {μ : Measure α} [IsFiniteMeasure μ] {ν : Measure γ} [IsProbabilityMeasure ν]
     (h : HasCondDistrib Y X κ μ) :
     HasCondDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) κ (μ.prod ν) where
-  aemeasurable_fst := by have := h.aemeasurable_fst; fun_prop
-  aemeasurable_snd := by have := h.aemeasurable_snd; fun_prop
-  condDistrib_eq := by
-    have : ((μ.prod ν).map (fun ω ↦ X ω.1)) = μ.map X := by
+  aemeasurable := by fun_prop
+  map_eq := by
+    have h_rhs : Measure.map (fun ω ↦ X ω.1) (μ.prod ν) ⊗ₘ κ = (μ.map X) ⊗ₘ κ := by
       conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst]
       rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)]
       · rfl
-      · have := h.aemeasurable_snd
+      · have := h.aemeasurable_fst
         simpa
-    rw [this]
-    exact (condDistrib_fst_prod X h.aemeasurable_fst ν).trans h.condDistrib_eq
-
-lemma HasCondDistrib.comp [IsFiniteMeasure μ]
-    (h : HasCondDistrib Y X κ μ) {f : Ω → Ω'} (hf : Measurable f) :
-    HasCondDistrib (fun ω ↦ f (Y ω)) X (κ.map f) μ where
-  aemeasurable_fst := by have := h.aemeasurable_fst; fun_prop
-  aemeasurable_snd := by have := h.aemeasurable_snd; fun_prop
-  condDistrib_eq := by
-    have h_comp := condDistrib_comp X (Y := Y) (f := f) (mβ := mβ) h.aemeasurable_fst hf
-    refine h_comp.trans ?_
-    have h' := h.condDistrib_eq
-    filter_upwards [h'] with ω hω
-    rw [Kernel.map_apply _ hf, hω, Kernel.map_apply _ hf]
-
-lemma HasCondDistrib.fst {Y : α → Ω × Ω'} {κ : Kernel β (Ω × Ω')} [IsFiniteMeasure μ]
-    (h : HasCondDistrib Y X κ μ) :
-    HasCondDistrib (fun ω ↦ (Y ω).1) X κ.fst μ := by
-  rw [Kernel.fst_eq]
-  exact HasCondDistrib.comp h measurable_fst
-
-lemma HasCondDistrib.snd {Y : α → Ω × Ω'} {κ : Kernel β (Ω × Ω')} [IsFiniteMeasure μ]
-    (h : HasCondDistrib Y X κ μ) :
-    HasCondDistrib (fun ω ↦ (Y ω).2) X κ.snd μ := by
-  rw [Kernel.snd_eq]
-  exact HasCondDistrib.comp h measurable_snd
-
--- TODO: Rename to `HasCondDistrib.comp_right`?
-lemma HasCondDistrib.comp_right' [IsFiniteMeasure μ] [IsFiniteKernel κ] {f : γ → β}
-    (hf : Measurable f) {Z : α → γ} (h : HasCondDistrib Y Z (κ.comap f hf) μ) :
-    HasCondDistrib Y (f ∘ Z) κ μ := by
-  have hY : AEMeasurable Y μ := h.aemeasurable_fst
-  have hZ : AEMeasurable Z μ := h.aemeasurable_snd
-  have hfZ : AEMeasurable (f ∘ Z) μ := hf.comp_aemeasurable hZ
-  refine ⟨hY, hfZ, ?_⟩
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ hY]
-  calc μ.map (fun a ↦ ((f ∘ Z) a, Y a))
-  _ = (μ.map (fun a ↦ (Z a, Y a))).map (Prod.map f id) := by
-      rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (hZ.prodMk hY)]
-      rfl
-  _ = (μ.map Z ⊗ₘ κ.comap f hf).map (Prod.map f id) := by
-      rw [(condDistrib_ae_eq_iff_measure_eq_compProd Z hY _).mp h.condDistrib_eq]
-  _ = (μ.map Z).map f ⊗ₘ κ := by
-      ext s hs
-      rw [Measure.map_apply (by fun_prop) hs, Measure.compProd_apply (by measurability),
-          Measure.compProd_apply hs, lintegral_map (Kernel.measurable_kernel_prodMk_left hs) hf]
-      rfl
-  _ = μ.map (f ∘ Z) ⊗ₘ κ := by
-      rw [AEMeasurable.map_map_of_aemeasurable hf.aemeasurable hZ]
-
-lemma HasCondDistrib.comp_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ)
-    (f : β ≃ᵐ γ) :
-    HasCondDistrib Y (f ∘ X) (κ.comap f.symm (by fun_prop) : Kernel γ Ω) μ := by
-  apply HasCondDistrib.comp_right' f.measurable
-  simpa [← Kernel.comap_comp_right]
+    rw [h_rhs, ← h.map_eq]
+    conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst]
+    rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)]
+    · rfl
+    · have := h.aemeasurable
+      simpa
 
 lemma HasCondDistrib.prod_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ)
     {f : β → γ} (hf : Measurable f) :
     HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ := by
-  have hY := h.aemeasurable_fst
-  have hX := h.aemeasurable_snd
-  refine ⟨h.aemeasurable_fst, by fun_prop, ?_⟩
-  have h_eq := h.condDistrib_eq
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop) _] at h_eq ⊢
+  refine ⟨by fun_prop, ?_⟩
+  have h_eq := h.map_eq
   calc μ.map (fun x ↦ ((X x, f (X x)), Y x))
   _ = (μ.map (fun ω ↦ (X ω, Y ω))).map (fun p ↦ ((p.1, f p.1), p.2)) := by
     rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
@@ -145,10 +81,8 @@ lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X
     have h_eq : X = (fun p ↦ p.1) ∘ (fun a ↦ (X a, f (X a))) := by ext; simp
     rw [h_eq]
     exact Measurable.comp_aemeasurable (by fun_prop) (by fun_prop)
-  have hY := h.aemeasurable_fst
-  refine ⟨by fun_prop, by fun_prop, ?_⟩
-  have h_eq := h.condDistrib_eq
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop) _] at h_eq ⊢
+  refine ⟨by fun_prop, ?_⟩
+  have h_eq := h.map_eq
   calc μ.map (fun x ↦ (X x, Y x))
   _ = (μ.map (fun ω ↦ ((X ω, f (X ω)), Y ω))).map (fun p ↦ (p.1.1, p.2)) := by
     rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
@@ -172,101 +106,79 @@ lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X
     rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
       Measure.map_dirac' (by fun_prop)]
 
-lemma HasCondDistrib.hasLaw_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q]
-    (h : HasCondDistrib Y X (Kernel.const β Q) μ) : HasLaw Y Q μ := by
-  obtain ⟨hY, hX, h⟩ := h
-  refine ⟨hY, ?_⟩
-  have h_snd : (μ.map (fun ω => (X ω, Y ω))).snd = Q := by
-    have h_map : μ.map (fun ω => (X ω, Y ω)) = (μ.map X) ⊗ₘ (Kernel.const _ Q) :=
-      have h_map : μ.map (fun ω => (X ω, Y ω)) = (μ.map X) ⊗ₘ (condDistrib Y X μ) :=
-      (compProd_map_condDistrib hY).symm
-      h_map.trans (Measure.compProd_congr h)
-    rw [h_map, MeasureTheory.Measure.snd_compProd]
-    simp [MeasureTheory.Measure.map_apply_of_aemeasurable hX]
-  rwa [Measure.snd_map_prodMk₀ hX] at h_snd
-
 lemma HasCondDistrib.indepFun_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q]
-    (h : HasCondDistrib Y X (Kernel.const β Q) μ) : IndepFun X Y μ := by
-  rw [indepFun_iff_condDistrib_eq_const h.aemeasurable_snd h.aemeasurable_fst,
-    h.hasLaw_of_const.map_eq]
-  exact h.condDistrib_eq
+    (h : HasCondDistrib Y X (Kernel.const β Q) μ) :
+    IndepFun X Y μ := by
+  rw [indepFun_iff_map_prod_eq_prod_map_map h.aemeasurable_fst h.aemeasurable_snd, h.map_eq,
+    h.hasLaw_of_const.map_eq, Measure.compProd_const]
 
 lemma HasCondDistrib.const_map_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q]
     (h : HasCondDistrib Y X (Kernel.const β Q) μ) [StandardBorelSpace β] [Nonempty β] :
     HasCondDistrib X Y (Kernel.const Ω (μ.map X)) μ where
-  aemeasurable_fst := h.aemeasurable_snd
-  aemeasurable_snd := h.aemeasurable_fst
-  condDistrib_eq :=
-    condDistrib_of_indepFun h.indepFun_of_const.symm h.aemeasurable_fst h.aemeasurable_snd
+  aemeasurable := by fun_prop
+  map_eq := by
+    calc μ.map (fun ω ↦ (Y ω, X ω))
+    _ = (μ.map (fun ω ↦ (X ω, Y ω))).map Prod.swap := by
+      rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
+      rfl
+    _ = (μ.map X ⊗ₘ Kernel.const β Q).map Prod.swap := by rw [h.map_eq]
+    _ = μ.map Y ⊗ₘ Kernel.const Ω (μ.map X) := by simp [h.hasLaw_of_const.map_eq, Measure.prod_swap]
 
 lemma HasLaw.prod_of_hasCondDistrib {P : Measure β} [IsFiniteMeasure μ] [IsSFiniteKernel κ]
     (h1 : HasLaw X P μ) (h2 : HasCondDistrib Y X κ μ) :
-    HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ := by
-  have hX := h1.aemeasurable
-  have hY := h2.aemeasurable_fst
-  refine ⟨by fun_prop, ?_⟩
-  rw [← compProd_map_condDistrib (by fun_prop), h1.map_eq]
-  refine Measure.compProd_congr ?_
-  rw [← h1.map_eq]
-  exact h2.condDistrib_eq
-
-lemma HasCondDistrib.of_compProd [IsFiniteMeasure μ] [IsFiniteKernel κ] {Z : α → Ω'}
-    {η : Kernel (β × Ω) Ω'} [IsMarkovKernel η]
-    (h : HasCondDistrib (fun a ↦ (Y a, Z a)) X (κ ⊗ₖ η) μ) :
-    HasCondDistrib Z (fun a ↦ (X a, Y a)) η μ := by
-  have hZ : AEMeasurable Z μ := h.aemeasurable_fst.snd
-  have hX : AEMeasurable X μ := h.aemeasurable_snd
-  have hY : AEMeasurable Y μ := h.aemeasurable_fst.fst
-  refine ⟨hZ, (hX.prodMk hY), ?_⟩
-  have hc := h.condDistrib_eq
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at hc ⊢
-  calc μ.map (fun a ↦ ((X a, Y a), Z a))
-  _ = (μ.map X ⊗ₘ (κ ⊗ₖ η)).map MeasurableEquiv.prodAssoc.symm := by
-      rw [← hc, AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
-      rfl
-  _ = μ.map X ⊗ₘ κ ⊗ₘ η :=
-      Measure.compProd_assoc
-  _ = μ.map (fun a ↦ (X a, Y a)) ⊗ₘ η := by
-      rw [← (condDistrib_ae_eq_iff_measure_eq_compProd X hY κ).1]
-      simpa using h.fst.condDistrib_eq
+    HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ :=
+  ⟨by fun_prop, by rw [h2.map_eq, h1.map_eq]⟩
 
 lemma HasCondDistrib.prod [IsFiniteMeasure μ] [IsFiniteKernel κ]
     {Z : α → Ω'} {η : Kernel (β × Ω) Ω'} [IsFiniteKernel η]
     (h1 : HasCondDistrib Y X κ μ) (h2 : HasCondDistrib Z (fun ω ↦ (X ω, Y ω)) η μ) :
     HasCondDistrib (fun ω ↦ (Y ω, Z ω)) X (κ ⊗ₖ η) μ := by
-  have hX := h1.aemeasurable_snd
-  have hY := h1.aemeasurable_fst
-  have hZ := h2.aemeasurable_fst
-  refine ⟨by fun_prop, by fun_prop, ?_⟩
-  have h_condDistrib_Y := h1.condDistrib_eq
-  have h_condDistrib_Z := h2.condDistrib_eq
-  have h_prod := condDistrib_prod_left hY hZ hX
-  have h_prod' : 𝓛[fun ω ↦ (Y ω, Z ω) | X; μ] =ᵐ[μ.map X] (κ ⊗ₖ 𝓛[Z | fun ω ↦ (X ω, Y ω); μ]) := by
-    filter_upwards [h_condDistrib_Y, h_prod] with ω hω₁ hω₂
-    rw [hω₂]
-    ext s hs
-    rw [Kernel.compProd_apply hs, Kernel.compProd_apply hs]
-    simp [hω₁]
-  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)]
-    at h_condDistrib_Z h_condDistrib_Y ⊢
-  rw [← Measure.compProd_assoc', ← h_condDistrib_Y, ← h_condDistrib_Z,
+  refine ⟨by fun_prop, ?_⟩
+  rw [← Measure.compProd_assoc', ← h1.map_eq, ← h2.map_eq,
     AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
   rfl
 
+lemma ae_eq_of_hasCondDistrib_deterministic [MeasurableEq Ω] [SFinite μ] {f : β → Ω}
+    (hf : Measurable f) (hX : AEMeasurable X μ)
+    (hY : AEMeasurable Y μ) (h : HasCondDistrib Y X (Kernel.deterministic f hf) μ) :
+    Y =ᵐ[μ] f ∘ X := by
+  refine ae_eq_of_map_prodMk_eq hf hX hY ?_
+  rw [h.map_eq, Measure.compProd_deterministic,
+    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
+  rfl
+
+variable [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace Ω'] [Nonempty Ω']
+
+lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
+    (h : HasCondDistrib Y X κ μ) :
+    condDistrib Y X μ =ᵐ[μ.map X] κ := by
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h.map_eq]
+
+lemma hasCondDistrib_of_condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
+    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
+    (h : condDistrib Y X μ =ᵐ[μ.map X] κ) :
+    HasCondDistrib Y X κ μ where
+  aemeasurable := by fun_prop
+  map_eq := by rw [← compProd_map_condDistrib hY, Measure.compProd_congr h]
+
 lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β]
-    {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω} {η : Kernel (γ × β) Ω} (hf : Measurable f)
+    {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω}
+    {η : Kernel (γ × β) Ω} [IsFiniteKernel η] (hf : Measurable f)
     (hg : Measurable g) (hW : AEMeasurable W μ)
     (hcd : HasCondDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) η μ) :
     ∀ᵐ z ∂(μ.map Z), HasCondDistrib g f (η.sectR z) (condDistrib W Z μ z) := by
+  suffices ∀ᵐ z ∂μ.map Z, condDistrib g f (condDistrib W Z μ z) =ᵐ[(condDistrib W Z μ z).map f]
+      (η.sectR z) by
+    filter_upwards [this] with z hz
+    exact hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) hz
   have h_eq : condDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) μ
       =ᵐ[μ.map Z ⊗ₘ (condDistrib W Z μ).map f] η := by
     rw [← Measure.compProd_congr (condDistrib_comp Z hW hf),
         compProd_map_condDistrib (hf.comp_aemeasurable hW)]
     exact hcd.condDistrib_eq
   filter_upwards [
-    condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_snd.fst,
+    condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_fst.fst,
     Measure.ae_ae_of_ae_compProd h_eq] with z hc ha
-  refine ⟨hg.aemeasurable, hf.aemeasurable, ?_⟩
   rw [Kernel.map_apply _ hf] at ha
   filter_upwards [hc, ha] with b hcb hab using hcb.trans hab
 

LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean

@@ -400,14 +400,14 @@ lemma indepFun_snd_prod (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (h_ind
   rfl
 
 -- cf. measurableSet_graph (Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean)
-lemma measurableSet_graph' {β Ω : Type*} [MeasurableSpace β] [MeasurableSpace Ω]
-    [StandardBorelSpace Ω] {f : β → Ω} (hf : Measurable f) :
-    MeasurableSet {p : β × Ω | p.2 = f p.1} := by
-  letI := upgradeStandardBorel Ω
-  exact (measurable_snd.prodMk (by fun_prop)) isClosed_diagonal.measurableSet
-
-omit [Nonempty Ω] [IsFiniteMeasure μ] in
-lemma ae_eq_of_map_prodMk_eq {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ)
+lemma measurableSet_graph' {β Ω : Type*} {_ : MeasurableSpace β} {_ : MeasurableSpace Ω}
+    [MeasurableEq Ω] {f : β → Ω} (hf : Measurable f) :
+    MeasurableSet {p : β × Ω | p.2 = f p.1} :=
+  measurableSet_eq_fun (by fun_prop) (by fun_prop)
+
+omit [IsFiniteMeasure μ] in
+lemma ae_eq_of_map_prodMk_eq {β Ω : Type*} {_ : MeasurableSpace β} {_ : MeasurableSpace Ω}
+    [MeasurableEq Ω] {X : α → β} {Y : α → Ω} {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ)
     (hY : AEMeasurable Y μ) (h : μ.map (fun ω ↦ (X ω, Y ω)) = μ.map (fun ω ↦ (X ω, f (X ω)))) :
     Y =ᵐ[μ] f ∘ X := by
   have hp : ∀ᵐ p ∂μ.map (fun ω ↦ (X ω, f (X ω))), p.2 = f p.1 :=

LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean

@@ -67,7 +67,7 @@ lemma MeasurableEquiv.coe_refl {α : Type*} {mα : MeasurableSpace α} :
     (MeasurableEquiv.refl α : α → α) = id := rfl
 
 set_option backward.isDefEq.respectTransparency false in
-lemma hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
+lemma hasLaw_Iic_of_forall_hasCondDistrib'
     {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N n : ℕ}
     (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P)
     (hn : n ≤ N) :
@@ -121,8 +121,7 @@ lemma hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [
     congr
     simp [MeasurableEquiv.coe_refl]
 
-lemma hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
-    {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P)
+lemma hasLaw_Iic_of_forall_hasCondDistrib {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P)
     (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P)
     (n : ℕ) :
     HasLaw (fun ω (i : Iic n) ↦ Y i ω)
@@ -136,27 +135,25 @@ lemma trajMeasure_map_frestrictLe (n : ℕ) :
   rw [trajMeasure, ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc,
     Kernel.deterministic_comp_eq_map, traj_map_frestrictLe]
 
-lemma eq_trajMeasure_map_frestrictLe [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
-    {Y : (n : ℕ) → Ω → X n}
-    (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ}
+lemma eq_trajMeasure_map_frestrictLe {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ}
     (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) :
     P.map (fun ω (n : Iic N) ↦ Y n ω) = (trajMeasure μ₀ κ).map (frestrictLe N) := by
   rw [(hasLaw_Iic_of_forall_hasCondDistrib' h0 h_condDistrib le_rfl).map_eq,
     trajMeasure_map_frestrictLe]
 
--- todo: switch to `HasLaw`
 /-- Uniqueness of `trajMeasure`. -/
-lemma eq_trajMeasure [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
-    {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n))
+lemma hasLaw_trajMeasure {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n))
     (h0 : HasLaw (Y 0) μ₀ P)
     (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) :
-    P.map (fun ω n ↦ Y n ω) = trajMeasure μ₀ κ := by
-  refine IsProjectiveLimit.unique (P := fun (J : Finset ℕ) ↦ P.map (fun ω (i : J) ↦ Y i ω)) ?_ ?_
-  · exact isProjectiveLimit_map (by fun_prop)
-  rw [isProjectiveLimit_nat_iff]
-  swap; · exact isProjectiveMeasureFamily_map_restrict (by fun_prop)
-  intro n
-  rw [(hasLaw_Iic_of_forall_hasCondDistrib h0 h_condDistrib n).map_eq,
-    trajMeasure_map_frestrictLe]
+    HasLaw (fun ω n ↦ Y n ω) (trajMeasure μ₀ κ) P where
+  aemeasurable := by fun_prop
+  map_eq := by
+    refine IsProjectiveLimit.unique (P := fun (J : Finset ℕ) ↦ P.map (fun ω (i : J) ↦ Y i ω)) ?_ ?_
+    · exact isProjectiveLimit_map (by fun_prop)
+    rw [isProjectiveLimit_nat_iff]
+    swap; · exact isProjectiveMeasureFamily_map_restrict (by fun_prop)
+    intro n
+    rw [(hasLaw_Iic_of_forall_hasCondDistrib h0 h_condDistrib n).map_eq,
+      trajMeasure_map_frestrictLe]
 
 end ProbabilityTheory.Kernel