Theorems · Theorem · probability

indepFun_of_bcf

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {G : Type u_6} {H : Type u_7}
  [inst : TopologicalSpace G] [inst_1 : MeasurableSpace G] [BorelSpace G] [HasOuterApproxClosed G]
  [inst_4 : TopologicalSpace H] [inst_5 : MeasurableSpace H] [BorelSpace H] [HasOuterApproxClosed H] {Z : Ω → G}
  {U : Ω → H} [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable Z P →
    AEMeasurable U P →
      (∀ (f : BoundedContinuousFunction G ℝ) (g : BoundedContinuousFunction H ℝ),
          ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P) →
        ProbabilityTheory.IndepFun Z U P

Two random variables $X$ and $Y$ are independent if for all real bounded continuous functions $f$ and $g$, $$P[f(X) g(Y)] = P[f(X)] * P[g(Y)].$$

Defined in

Mathlib.Probability.Independence.BoundedContinuousFunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsFiniteMeasure