Theorems · Theorem · probability

indepFun_process_of_prod_bcf

∀ {Ω : Type u_1} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {F : T → Type u_5} {G : Type u_6}
  [inst : (t : T) → TopologicalSpace (F t)] [inst_1 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)]
  [∀ (t : T), HasOuterApproxClosed (F t)] [inst_4 : TopologicalSpace G] [inst_5 : MeasurableSpace G] [BorelSpace G]
  [HasOuterApproxClosed G] {Y : (t : T) → Ω → F t} {Z : Ω → G} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  AEMeasurable Z P →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : BoundedContinuousFunction G ℝ) (J : Finset T) (g : (t : ↥J) → BoundedContinuousFunction (F ↑t) ℝ),
          ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y ↑t) x ∂P =
            (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y ↑t) x ∂P) →
        ProbabilityTheory.IndepFun Z (fun ω t => Y t ω) 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