Independence of stochastic processes

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.indepFun_process {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {α : Type u_3} {mα : MeasurableSpace α} {κ : Kernel α Ω} {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) [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.iIndepFun.iIndepFun_process {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {α : Type u_3} {mα : MeasurableSpace α} {κ : Kernel α Ω} {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.IndepFun.indepFun_process {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : Type u_3} {𝓧 : S → Type u_4} {𝓨 : T → Type u_5} [(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.IsProbabilityMeasure 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.iIndepFun.iIndepFun_process {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : S → Type u_3} {𝓧 : (i : S) → T i → Type u_4} [(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.