Theorems · Theorem · probability

ProbabilityTheory.IndepFun.indepFun_process

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

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasureTheory.IsZeroOrProbabilityMeasure