Theorems · Theorem · probability

ProbabilityTheory.indepFun_iff_hasLaw_prodMk_prod

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {𝓨 : Type u_3}
  {m𝓨 : MeasurableSpace 𝓨} {ν : MeasureTheory.Measure 𝓨} {Y : Ω → 𝓨},
  ProbabilityTheory.HasLaw X μ P →
    ProbabilityTheory.HasLaw Y ν P →
      (ProbabilityTheory.IndepFun X Y P ↔ ProbabilityTheory.HasLaw (fun ω => (X ω, Y ω)) (μ.prod ν) P)

Defined in

Mathlib.Probability.HasLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure