Theorems · Theorem · probability

ProbabilityTheory.indepFun_of_identDistrib_pair

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSpace δ] {μ : MeasureTheory.Measure γ} {μ' : MeasureTheory.Measure δ}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure μ'] {X : γ → α} {X' : δ → α} {Y : γ → β}
  {Y' : δ → β},
  ProbabilityTheory.IndepFun X Y μ →
    ProbabilityTheory.IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ' →
      ProbabilityTheory.IndepFun X' Y' μ'

If X and Y are independent and (X, Y) and (X', Y') are identically distributed, then X' and Y' are independent.

Defined in

Mathlib.Probability.IdentDistrib

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasurableSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure