Theorems · Theorem · probability

ProbabilityTheory.Kernel.IndepFun.process_congr_left

∀ {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 X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) Y κ P →
    (∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) → ProbabilityTheory.Kernel.IndepFun (fun ω i => X' i ω) Y κ P

If X is a process independent from Y and for all i, X' i is almost everywhere equal to X i, then X' is also independent from Y. This implies that independence results about measurable processes should generally also hold for processes whose marginals are only a.e.-measurable.

Defined in

Mathlib.Probability.Independence.Process.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace