Theorems · Theorem · probability

ProbabilityTheory.IndepFun.process_congr

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

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace