feat: independence from a stochastic process (leanprover-community#31050)

Prove that a stochastic process $(X\_s)\_{s \in S}$ is independent from a random variable $Y$ if for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$. Use this to refactor proofs.

Author: EtienneC30

Mathlib/Probability/Independence/Process.lean

@@ -9,10 +9,13 @@ import Mathlib.Probability.Independence.Basic
 /-!
 # Independence of stochastic processes
 
+We prove that a stochastic process $(X_s)_{s \in S}$ is independent from a random variable $Y$ if
+for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$.
+
 We prove that two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
 for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
-$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent. We prove an analogous
-condition for a family of stochastic processes.
+$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent.
+We prove an analogous condition for a family of stochastic processes.
 
 ## Tags
 
@@ -29,15 +32,14 @@ namespace Kernel
 
 variable {α : Type*} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : Measure α}
 
-/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
-for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
-$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent. -/
-lemma IndepFun.indepFun_process {T : Type*} {𝓧 : S → Type*} {𝓨 : T → Type*}
-    [∀ i, MeasurableSpace (𝓧 i)] [∀ j, MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i}
-    {Y : (j : T) → Ω → 𝓨 j} (hX : ∀ i, Measurable (X i)) (hY : ∀ j, Measurable (Y j))
-    (h : ∀ (I : Finset S) (J : Finset T),
-      IndepFun (fun ω (i : I) ↦ X i ω) (fun ω (j : J) ↦ Y j ω) κ P) [IsZeroOrMarkovKernel κ] :
-    IndepFun (fun ω i ↦ X i ω) (fun ω j ↦ Y j ω) κ P := by
+/-- A stochastic process $(X_s)_{s \in S}$ is independent from a random variable $Y$ if
+for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$. -/
+lemma IndepFun.process_indepFun {𝓧 : S → Type*} {𝓨 : Type*}
+    [∀ i, MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i}
+    {Y : Ω → 𝓨} (hX : ∀ i, Measurable (X i)) (hY : Measurable Y)
+    (h : ∀ (I : Finset S),
+      IndepFun (fun ω (i : I) ↦ X i ω) Y κ P) [IsZeroOrMarkovKernel κ] :
+    IndepFun (fun ω i ↦ X i ω) Y κ P := by
   -- The π-system obtained by pulling back the π-system of square cylinders by `X`.
   let πX := {s : Set Ω | ∃ t ∈ squareCylinders (fun i ↦ {s : Set (𝓧 i) | MeasurableSet s}),
       (fun ω i ↦ X i ω) ⁻¹' t = s}
@@ -46,30 +48,43 @@ lemma IndepFun.indepFun_process {T : Type*} {𝓧 : S → Type*} {𝓨 : T → T
   have πX_gen : (MeasurableSpace.pi.comap fun ω i ↦ X i ω) = generateFrom πX := by
     rw [generateFrom_squareCylinders.symm, MeasurableSpace.comap_generateFrom]
     rfl
-  -- The π-system obtained by pulling back the π-system of square cylinders by `Y`.
-  let πY := {s : Set Ω | ∃ t ∈ squareCylinders (fun j ↦ {s : Set (𝓨 j) | MeasurableSet s}),
-      (fun ω j ↦ Y j ω) ⁻¹' t = s}
-  have πY_pi : IsPiSystem πY :=
-    IsPiSystem.comap (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp)) _
-  have πY_gen : (MeasurableSpace.pi.comap fun ω j ↦ Y j ω) = generateFrom πY := by
-    rw [generateFrom_squareCylinders.symm, MeasurableSpace.comap_generateFrom]
-    rfl
-  -- To prove independence, we prove independence of the generating π-systems.
-  refine IndepSets.indep (measurable_pi_iff.2 hX).comap_le (measurable_pi_iff.2 hY).comap_le
-     πX_pi πY_pi πX_gen πY_gen ?_
-  rintro - - ⟨-, ⟨I, s, hs, rfl⟩, rfl⟩ ⟨-, ⟨J, t, ht, rfl⟩, rfl⟩
-  simp only [Set.mem_pi, Set.mem_univ, Set.mem_setOf_eq, forall_const] at hs ht
-  have : (fun ω i ↦ X i ω) ⁻¹' .pi I s ∩ (fun ω j ↦ Y j ω) ⁻¹' .pi J t =
-      (fun ω (i : I) ↦ X i ω) ⁻¹' .pi (SetLike.coe Finset.univ) (fun i ↦ s i) ∩
-      (fun ω (j : J) ↦ Y j ω) ⁻¹' .pi (SetLike.coe Finset.univ) (fun j ↦ t j) := by
+  -- To prove independence, we prove independence of the generating π-system with the `σ`-alebra.
+  refine IndepSets.indep (measurable_pi_iff.2 hX).comap_le hY.comap_le
+    πX_pi (@isPiSystem_measurableSet Ω (.comap Y inferInstance)) πX_gen
+    (@generateFrom_measurableSet Ω (.comap Y inferInstance)).symm ?_
+  rintro - - ⟨-, ⟨I, s, hs, rfl⟩, rfl⟩ ⟨t, ht, rfl⟩
+  simp only [Set.mem_pi, Set.mem_univ, Set.mem_setOf_eq, forall_const] at hs
+  have : (fun ω i ↦ X i ω) ⁻¹' .pi I s =
+      (fun ω (i : I) ↦ X i ω) ⁻¹' .pi (SetLike.coe Finset.univ) (fun i ↦ s i)
+       := by
     ext; simp
   have h1 : MeasurableSet <| .pi (SetLike.coe Finset.univ) (fun (i : I) ↦ s i) :=
     .pi (Finset.countable_toSet _) (fun _ _ ↦ hs _)
-  have h2 : MeasurableSet <| .pi (SetLike.coe Finset.univ) (fun (j : J) ↦ t j) :=
-    .pi (Finset.countable_toSet _) (fun _ _ ↦ ht _)
-  filter_upwards [(h I J).measure_inter_preimage_eq_mul _ _ h1 h2] with ω hω
+  filter_upwards [(h I).measure_inter_preimage_eq_mul _ _ h1 ht] with ω hω
   rw [this, hω]
-  congr 2 <;> ext <;> simp
+
+/-- A random variable $X$ is independent from a stochastic process $(Y_s)_{s \in S}$  if
+for all $s_1, ..., s_p \in S$ the variable $Y$ is independent from the family
+$(X_{s_1}, ..., X_{s_p})$. -/
+lemma IndepFun.indepFun_process {𝓧 : Type*} {𝓨 : S → Type*}
+    [MeasurableSpace 𝓧] [∀ i, MeasurableSpace (𝓨 i)] {X : Ω → 𝓧}
+    {Y : (i : S) → Ω → 𝓨 i} (hX : Measurable X) (hY : ∀ i, Measurable (Y i))
+    (h : ∀ (I : Finset S),
+      IndepFun X (fun ω (i : I) ↦ Y i ω) κ P) [IsZeroOrMarkovKernel κ] :
+    IndepFun X (fun ω i ↦ Y i ω) κ P :=
+  (IndepFun.process_indepFun hY hX (fun I ↦ (h I).symm)).symm
+
+/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
+for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
+$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent. -/
+lemma IndepFun.process_indepFun_process {T : Type*} {𝓧 : S → Type*} {𝓨 : T → Type*}
+    [∀ i, MeasurableSpace (𝓧 i)] [∀ j, MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i}
+    {Y : (j : T) → Ω → 𝓨 j} (hX : ∀ i, Measurable (X i)) (hY : ∀ j, Measurable (Y j))
+    (h : ∀ (I : Finset S) (J : Finset T),
+      IndepFun (fun ω (i : I) ↦ X i ω) (fun ω (j : J) ↦ Y j ω) κ P) [IsZeroOrMarkovKernel κ] :
+    IndepFun (fun ω i ↦ X i ω) (fun ω j ↦ Y j ω) κ P := by
+  refine IndepFun.process_indepFun hX (measurable_pi_lambda _ hY) fun I ↦ ?_
+  exact IndepFun.indepFun_process (measurable_pi_lambda _ fun _ ↦ hX _) hY fun J ↦ h I J
 
 /-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
 for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}^ the families
@@ -117,16 +132,41 @@ end Kernel
 
 variable {P : Measure Ω}
 
+/-- A stochastic process $(X_s)_{s \in S}$ is independent from a random variable $Y$ if
+for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$. -/
+lemma IndepFun.process_indepFun {𝓧 : S → Type*} {𝓨 : Type*}
+    [∀ i, MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i}
+    {Y : Ω → 𝓨} (hX : ∀ i, Measurable (X i)) (hY : AEMeasurable Y P)
+    (h : ∀ (I : Finset S),
+      IndepFun (fun ω (i : I) ↦ X i ω) Y P) [IsZeroOrProbabilityMeasure P] :
+    IndepFun (fun ω i ↦ X i ω) Y P := by
+  suffices (fun ω i ↦ X i ω) ⟂ᵢ[P] (hY.mk Y) from
+    this.congr .rfl hY.ae_eq_mk.symm
+  exact Kernel.IndepFun.process_indepFun hX hY.measurable_mk (fun I ↦ (h I).congr .rfl hY.ae_eq_mk)
+
+/-- A random variable $X$ is independent from a stochastic process $(Y_s)_{s \in S}$  if
+for all $s_1, ..., s_p \in S$ the variable $Y$ is independent from the family
+$(X_{s_1}, ..., X_{s_p})$. -/
+lemma IndepFun.indepFun_process {𝓧 : Type*} {𝓨 : S → Type*}
+    [MeasurableSpace 𝓧] [∀ i, MeasurableSpace (𝓨 i)] {X : Ω → 𝓧}
+    {Y : (i : S) → Ω → 𝓨 i} (hX : AEMeasurable X P) (hY : ∀ i, Measurable (Y i))
+    (h : ∀ (I : Finset S),
+      IndepFun X (fun ω (i : I) ↦ Y i ω) P) [IsZeroOrProbabilityMeasure P] :
+    IndepFun X (fun ω i ↦ Y i ω) P := by
+  suffices (hX.mk X) ⟂ᵢ[P] (fun ω i ↦ Y i ω) from
+    this.congr hX.ae_eq_mk.symm .rfl
+  exact Kernel.IndepFun.indepFun_process hX.measurable_mk hY (fun I ↦ (h I).congr hX.ae_eq_mk .rfl)
+
 /-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
 for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
 $(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent. -/
-lemma IndepFun.indepFun_process {T : Type*} {𝓧 : S → Type*} {𝓨 : T → Type*}
+lemma IndepFun.process_indepFun_process {T : Type*} {𝓧 : S → Type*} {𝓨 : T → Type*}
     [∀ i, MeasurableSpace (𝓧 i)] [∀ j, MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i}
     {Y : (j : T) → Ω → 𝓨 j} (hX : ∀ i, Measurable (X i)) (hY : ∀ j, Measurable (Y j))
     (h : ∀ (I : Finset S) (J : Finset T),
-      IndepFun (fun ω (i : I) ↦ X i ω) (fun ω (j : J) ↦ Y j ω) P) [IsProbabilityMeasure P] :
+      IndepFun (fun ω (i : I) ↦ X i ω) (fun ω (j : J) ↦ Y j ω) P) [IsZeroOrProbabilityMeasure P] :
     IndepFun (fun ω i ↦ X i ω) (fun ω j ↦ Y j ω) P :=
-  Kernel.IndepFun.indepFun_process hX hY h
+  Kernel.IndepFun.process_indepFun_process hX hY h
 
 /-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
 for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}^ the families
@@ -135,8 +175,7 @@ $(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ...,
 lemma iIndepFun.iIndepFun_process {T : S → Type*} {𝓧 : (i : S) → (j : T i) → Type*}
     [∀ i j, MeasurableSpace (𝓧 i j)] {X : (i : S) → (j : T i) → Ω → 𝓧 i j}
     (hX : ∀ i j, Measurable (X i j))
-    (h : ∀ (I : Finset S) (J : (i : I) → Finset (T i)),
-      iIndepFun (fun i ω (j : J i) ↦ X i j ω) P) :
+    (h : ∀ (I : Finset S) (J : (i : I) → Finset (T i)), iIndepFun (fun i ω (j : J i) ↦ X i j ω) P) :
     iIndepFun (fun i ω j ↦ X i j ω) P :=
   Kernel.iIndepFun.iIndepFun_process hX h