Theorems · Theorem · probability

ProbabilityTheory.Kernel.IndepFun.process_indepFun_process

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

Defined in

Mathlib.Probability.Independence.Process.Basic

Cited by

2 results in Mathlib

Foundations

Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpaceProbabilityTheory.IsZeroOrMarkovKernel