Theorems · Theorem · probability

indepSets_comap_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] {𝒜 : Set (Set Ω)},
  (∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P) →
    AEMeasurable Z P →
      (∀ A ∈ 𝒜, ∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P) →
        ProbabilityTheory.IndepSets 𝒜 {A | MeasurableSet A} P

Defined in

Mathlib.Probability.Independence.BoundedContinuousFunction

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsProbabilityMeasure