Theorems · Theorem · probability

ProbabilityTheory.Kernel.IndepFun.indepFun_process

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

Defined in

Mathlib.Probability.Independence.Process.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceProbabilityTheory.IsZeroOrMarkovKernel