Theorems · Theorem · probability

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} [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.IndepFun (fun ω i => X (↑i) ω) (fun ω j => Y (↑j) ω) P) →
        ∀ [MeasureTheory.IsZeroOrProbabilityMeasure P],
          ProbabilityTheory.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

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasureTheory.IsZeroOrProbabilityMeasure