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_indepFun {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {α : Type u_3} {mα : MeasurableSpace α} {κ : Kernel α Ω} {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) [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.indepFun_process {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {α : Type u_3} {mα : MeasurableSpace α} {κ : Kernel α Ω} {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) [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.process_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.process_indepFun {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_3} {𝓨 : Type u_4} [(i : S) → MeasurableSpace (𝓧 i)] [MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨} (hX : ∀ (i : S), Measurable (X i)) (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$.

theorem ProbabilityTheory.IndepFun.indepFun_process {S : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : Type u_3} {𝓨 : S → Type u_4} [MeasurableSpace 𝓧] [(i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i} (hX : AEMeasurable X P) (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.process_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.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.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.