Theorems · Theorem · probability

ProbabilityTheory.Kernel.IndepFun.process_indepFun

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

Defined in

Mathlib.Probability.Independence.Process.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceProbabilityTheory.IsZeroOrMarkovKernel