Theorems · Theorem · probability

ProbabilityTheory.Kernel.IndepFun.process_congr

∀ {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : T → Type u_6}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : (j : T) → MeasurableSpace (𝓨 j)] {X X' : (i : S) → Ω → 𝓧 i}
  {Y Y' : (j : T) → Ω → 𝓨 j},
  ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) κ P →
    (∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) →
      (∀ (j : T), ∀ᵐ (a : α) ∂P, Y j =ᵐ[κ a] Y' j) →
        ProbabilityTheory.Kernel.IndepFun (fun ω i => X' i ω) (fun ω j => Y' j ω) κ P

If X and Y are two independent processes and for all i, X' i is almost everywhere equal to X i, and for all j, Y' j is almost everywhere equal to Y j, then X' is 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

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace