Theorems · Theorem · probability

indicator_indepFun_pi_of_bcf

∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P] [Finite S]
  {A : Set Ω},
  MeasureTheory.NullMeasurableSet A P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ),
          ∫ (ω : Ω) in A, f fun x => X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x => X x ω ∂P) →
        ProbabilityTheory.IndepFun (A.indicator 1) (fun ω s => X s ω) P

The indicator of a set $A$ and a family of random variables $(X_1, ..., X_p)$ are independent if for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X_1, ..., X_p)] = P(A) P[f(X_1, ..., X_p)].$$

Defined in

Mathlib.Probability.Independence.BoundedContinuousFunction

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsProbabilityMeasureFinite