Theorems · Theorem · probability

process_indepFun_of_prod_bcf

∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4} {H : Type u_7}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : TopologicalSpace H] [inst_5 : MeasurableSpace H] [BorelSpace H]
  [HasOuterApproxClosed H] {X : (s : S) → Ω → E s} {U : Ω → H} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    AEMeasurable U P →
      (∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ) (g : BoundedContinuousFunction H ℝ),
          ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X ↑s) * ⇑g ∘ U) x ∂P =
            (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) U P

Defined in

Mathlib.Probability.Independence.BoundedContinuousFunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsZeroOrProbabilityMeasure