Theorems · Theorem · probability

indicator_indepFun_of_bcf

∀ {Ω : Type u_1} {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] {A : Set Ω},
  MeasureTheory.NullMeasurableSet A P →
    AEMeasurable Z P →
      (∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P) →
        ProbabilityTheory.IndepFun (A.indicator 1) Z P

The indicator of a set $A$ and a random variable $X$ are independent if 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

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsProbabilityMeasure