Theorems · Theorem · probability

indep_comap_of_bcf

∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {G : Type u_6} [inst : TopologicalSpace G]
  [inst_1 : MeasurableSpace G] [BorelSpace G] [HasOuterApproxClosed G] {Z : Ω → G}
  [MeasureTheory.IsProbabilityMeasure P],
  m ≤ mΩ →
    AEMeasurable Z P →
      (∀ (A : Set Ω),
          MeasurableSet A →
            ∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P) →
        ProbabilityTheory.Indep m (MeasurableSpace.comap Z inferInstance) P

A sigma-algebra $\mathcal{A}$ and a random variable $X$ are independent if for all set $A \in \mathcal{A}$ and for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X)] = P(A) P[f(X)].$$

Defined in

Mathlib.Probability.Independence.BoundedContinuousFunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsProbabilityMeasure