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.

Tags

independence, stochastic processes

theorem ProbabilityTheory.Kernel.IndepFun.process_congr_left {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (h1 : IndepFun (fun (ω : Ω) (i : S) => X i ω) Y κ P) (h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) : IndepFun (fun (ω : Ω) (i : S) => X' i ω) Y κ P

If X is a process independent from Y and for all i, X' i is almost everywhere equal to X i, then X' is also independent from Y. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.Kernel.IndepFun.process_congr_right {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (h1 : IndepFun Y (fun (ω : Ω) (i : S) => X i ω) κ P) (h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) : IndepFun Y (fun (ω : Ω) (i : S) => X' i ω) κ P

If X is a process independent from Y and for all i, X' i is almost everywhere equal to X i, then X' is also independent from Y. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.Kernel.IndepFun.process_congr {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : T → Type u_6} [(i : S) → MeasurableSpace (𝓧 i)] [(j : T) → MeasurableSpace (𝓨 j)] {X X' : (i : S) → Ω → 𝓧 i} {Y Y' : (j : T) → Ω → 𝓨 j} (hXY : IndepFun (fun (ω : Ω) (i : S) => X i ω) (fun (ω : Ω) (j : T) => Y j ω) κ P) (hX : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) (hY : ∀ (j : T), ∀ᵐ (a : α) ∂P, Y j =ᵐ[κ a] Y' j) : IndepFun (fun (ω : Ω) (i : S) => X' i ω) (fun (ω : Ω) (j : T) => Y' j ω) κ P

If X and Y are two independent processes and for all i, X' i is almost everywhere equal to X i, and for all j, Y' j is almost everywhere equal to Y j, then X' is independent from Y'. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.Kernel.IndepFun.process_indepFun {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (hX : ∀ (i : S), Measurable (X i)) (hY : Measurable Y) (h : ∀ (I : Finset S), IndepFun (fun (ω : Ω) (i : ↥I) => X (↑i) ω) Y κ P) [IsZeroOrMarkovKernel κ] : IndepFun (fun (ω : Ω) (i : S) => X i ω) Y κ P

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$.

theorem ProbabilityTheory.Kernel.IndepFun.process_indepFun₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (hX : ∀ (i : S), AEMeasurable (X i) (P.bind ⇑κ)) (hY : AEMeasurable Y (P.bind ⇑κ)) (h : ∀ (I : Finset S), IndepFun (fun (ω : Ω) (i : ↥I) => X (↑i) ω) Y κ P) [IsZeroOrMarkovKernel κ] : IndepFun (fun (ω : Ω) (i : S) => X i ω) Y κ P

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$.

This version only requires a.e.-measurability.

theorem ProbabilityTheory.Kernel.IndepFun.indepFun_process {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : Type u_5} {𝓨 : S → Type u_6} [MeasurableSpace 𝓧] [(i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i} (hX : Measurable X) (hY : ∀ (i : S), Measurable (Y i)) (h : ∀ (I : Finset S), IndepFun X (fun (ω : Ω) (i : ↥I) => Y (↑i) ω) κ P) [IsZeroOrMarkovKernel κ] : IndepFun X (fun (ω : Ω) (i : S) => Y i ω) κ P

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})$.

theorem ProbabilityTheory.Kernel.IndepFun.indepFun_process₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : Type u_5} {𝓨 : S → Type u_6} [MeasurableSpace 𝓧] [(i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i} (hX : AEMeasurable X (P.bind ⇑κ)) (hY : ∀ (i : S), AEMeasurable (Y i) (P.bind ⇑κ)) (h : ∀ (I : Finset S), IndepFun X (fun (ω : Ω) (i : ↥I) => Y (↑i) ω) κ P) [IsZeroOrMarkovKernel κ] : IndepFun X (fun (ω : Ω) (i : S) => Y i ω) κ P

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})$.

This version only requires a.e.-measurability.

theorem ProbabilityTheory.Kernel.IndepFun.process_indepFun_process {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {T : Type u_5} {𝓧 : S → Type u_6} {𝓨 : T → Type u_7} [(i : S) → MeasurableSpace (𝓧 i)] [(j : T) → MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i} {Y : (j : T) → Ω → 𝓨 j} (hX : ∀ (i : S), Measurable (X i)) (hY : ∀ (j : T), 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 : S) => X i ω) (fun (ω : Ω) (j : T) => Y j ω) κ P

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.

theorem ProbabilityTheory.Kernel.IndepFun.process_indepFun_process₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {T : Type u_5} {𝓧 : S → Type u_6} {𝓨 : T → Type u_7} [(i : S) → MeasurableSpace (𝓧 i)] [(j : T) → MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i} {Y : (j : T) → Ω → 𝓨 j} (hX : ∀ (i : S), AEMeasurable (X i) (P.bind ⇑κ)) (hY : ∀ (j : T), AEMeasurable (Y j) (P.bind ⇑κ)) (h : ∀ (I : Finset S) (J : Finset T), IndepFun (fun (ω : Ω) (i : ↥I) => X (↑i) ω) (fun (ω : Ω) (j : ↥J) => Y (↑j) ω) κ P) [IsZeroOrMarkovKernel κ] : IndepFun (fun (ω : Ω) (i : S) => X i ω) (fun (ω : Ω) (j : T) => Y j ω) κ P

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.

This version only requires a.e.-measurability.

theorem ProbabilityTheory.Kernel.iIndepFun.process_congr {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {T : S → Type u_5} {𝓧 : (i : S) → T i → Type u_6} [(i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X X' : (i : S) → (j : T i) → Ω → 𝓧 i j} (h1 : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X i j ω) κ P) (h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j) : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X' i j ω) κ P

If stochastic processes X : (i : S) → (j : T i) → Ω → 𝓧 i j are independent and for all i j, X' i j is almost everywhere equal to X i j, then X' are also independent. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {T : S → Type u_5} {𝓧 : (i : S) → T i → Type u_6} [(i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X : (i : S) → (j : T i) → Ω → 𝓧 i j} (hX : ∀ (i : S) (j : T i), Measurable (X i j)) (h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) => X (↑i) (↑j) ω) κ P) : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X i j ω) κ P

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 $(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ..., (X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.

theorem ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α} {κ : Kernel α Ω} {P : MeasureTheory.Measure α} {T : S → Type u_5} {𝓧 : (i : S) → T i → Type u_6} [(i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X : (i : S) → (j : T i) → Ω → 𝓧 i j} (hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (P.bind ⇑κ)) (h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) => X (↑i) (↑j) ω) κ P) : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X i j ω) κ P

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 $(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ..., (X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.

This version only requires a.e.-measurability.

theorem ProbabilityTheory.IndepFun.process_congr_left {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (h1 : IndepFun (fun (ω : Ω) (i : S) => X i ω) Y P) (h2 : ∀ (i : S), X i =ᵐ[P] X' i) : IndepFun (fun (ω : Ω) (i : S) => X' i ω) Y P

If X is a process independent from Y and for all i, X' i is almost everywhere equal to X i, then X' is also independent from Y. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.IndepFun.process_congr_right {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (h1 : IndepFun Y (fun (ω : Ω) (i : S) => X i ω) P) (h2 : ∀ (i : S), X i =ᵐ[P] X' i) : IndepFun Y (fun (ω : Ω) (i : S) => X' i ω) P

If X is a process independent from Y and for all i, X' i is almost everywhere equal to X i, then X' is also independent from Y. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.IndepFun.process_congr {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : T → Type u_5} [(i : S) → MeasurableSpace (𝓧 i)] [(j : T) → MeasurableSpace (𝓨 j)] {X X' : (i : S) → Ω → 𝓧 i} {Y Y' : (j : T) → Ω → 𝓨 j} (hXY : IndepFun (fun (ω : Ω) (i : S) => X i ω) (fun (ω : Ω) (j : T) => Y j ω) P) (hX : ∀ (i : S), X i =ᵐ[P] X' i) (hY : ∀ (j : T), Y j =ᵐ[P] Y' j) : IndepFun (fun (ω : Ω) (i : S) => X' i ω) (fun (ω : Ω) (j : T) => Y' j ω) P

If X and Y are two independent processes and for all i, X' i is almost everywhere equal to X i, and for all j, Y' j is almost everywhere equal to Y j, then X' is independent from Y'. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.IndepFun.process_indepFun {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (hX : ∀ (i : S), Measurable (X i)) (hY : Measurable Y) (h : ∀ (I : Finset S), IndepFun (fun (ω : Ω) (i : ↥I) => X (↑i) ω) Y P) [MeasureTheory.IsZeroOrProbabilityMeasure P] : IndepFun (fun (ω : Ω) (i : S) => X i ω) Y P

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$.

theorem ProbabilityTheory.IndepFun.process_indepFun₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (hX : ∀ (i : S), AEMeasurable (X i) P) (hY : AEMeasurable Y P) (h : ∀ (I : Finset S), IndepFun (fun (ω : Ω) (i : ↥I) => X (↑i) ω) Y P) [MeasureTheory.IsZeroOrProbabilityMeasure P] : IndepFun (fun (ω : Ω) (i : S) => X i ω) Y P

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$.

This version only requires a.e.-measurability.

theorem ProbabilityTheory.IndepFun.indepFun_process {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : Type u_4} {𝓨 : S → Type u_5} [MeasurableSpace 𝓧] [(i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i} (hX : Measurable X) (hY : ∀ (i : S), Measurable (Y i)) (h : ∀ (I : Finset S), IndepFun X (fun (ω : Ω) (i : ↥I) => Y (↑i) ω) P) [MeasureTheory.IsZeroOrProbabilityMeasure P] : IndepFun X (fun (ω : Ω) (i : S) => Y i ω) P

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})$.

theorem ProbabilityTheory.IndepFun.indepFun_process₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : Type u_4} {𝓨 : S → Type u_5} [MeasurableSpace 𝓧] [(i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i} (hX : AEMeasurable X P) (hY : ∀ (i : S), AEMeasurable (Y i) P) (h : ∀ (I : Finset S), IndepFun X (fun (ω : Ω) (i : ↥I) => Y (↑i) ω) P) [MeasureTheory.IsZeroOrProbabilityMeasure P] : IndepFun X (fun (ω : Ω) (i : S) => Y i ω) P

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})$.

This version only requires a.e.-measurability.

theorem ProbabilityTheory.IndepFun.process_indepFun_process {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : Type u_4} {𝓧 : S → Type u_5} {𝓨 : T → Type u_6} [(i : S) → MeasurableSpace (𝓧 i)] [(j : T) → MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i} {Y : (j : T) → Ω → 𝓨 j} (hX : ∀ (i : S), Measurable (X i)) (hY : ∀ (j : T), Measurable (Y j)) (h : ∀ (I : Finset S) (J : Finset T), IndepFun (fun (ω : Ω) (i : ↥I) => X (↑i) ω) (fun (ω : Ω) (j : ↥J) => Y (↑j) ω) P) [MeasureTheory.IsZeroOrProbabilityMeasure P] : IndepFun (fun (ω : Ω) (i : S) => X i ω) (fun (ω : Ω) (j : T) => Y j ω) P

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.

theorem ProbabilityTheory.IndepFun.process_indepFun_process₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : Type u_4} {𝓧 : S → Type u_5} {𝓨 : T → Type u_6} [(i : S) → MeasurableSpace (𝓧 i)] [(j : T) → MeasurableSpace (𝓨 j)] {X : (i : S) → Ω → 𝓧 i} {Y : (j : T) → Ω → 𝓨 j} (hX : ∀ (i : S), AEMeasurable (X i) P) (hY : ∀ (j : T), AEMeasurable (Y j) P) (h : ∀ (I : Finset S) (J : Finset T), IndepFun (fun (ω : Ω) (i : ↥I) => X (↑i) ω) (fun (ω : Ω) (j : ↥J) => Y (↑j) ω) P) [MeasureTheory.IsZeroOrProbabilityMeasure P] : IndepFun (fun (ω : Ω) (i : S) => X i ω) (fun (ω : Ω) (j : T) => Y j ω) P

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.

This version only requires a.e.-measurability.

theorem ProbabilityTheory.iIndepFun.process_congr {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_4} {𝓧 : (i : S) → T i → Type u_5} [(i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X X' : (i : S) → (j : T i) → Ω → 𝓧 i j} (h1 : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X i j ω) P) (h2 : ∀ (i : S) (j : T i), X i j =ᵐ[P] X' i j) : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X' i j ω) P

If stochastic processes X : (i : S) → (j : T i) → Ω → 𝓧 i j are independent and for all i j, X' i j is almost everywhere equal to X i j, then X' are also independent. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

theorem ProbabilityTheory.iIndepFun.iIndepFun_process {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_4} {𝓧 : (i : S) → T i → Type u_5} [(i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X : (i : S) → (j : T i) → Ω → 𝓧 i j} (hX : ∀ (i : S) (j : T i), Measurable (X i j)) (h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) => X (↑i) (↑j) ω) P) : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X i j ω) P

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 $(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ..., (X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.

theorem ProbabilityTheory.iIndepFun.iIndepFun_process₀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_4} {𝓧 : (i : S) → T i → Type u_5} [(i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X : (i : S) → (j : T i) → Ω → 𝓧 i j} (hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) P) (h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) => X (↑i) (↑j) ω) P) : iIndepFun (fun (i : S) (ω : Ω) (j : T i) => X i j ω) P

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 $(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ..., (X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.

This version only requires a.e.-measurability.