Theorems · Theorem · probability

indepFun_pi_of_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.IsFiniteMeasure P] [Finite T],
  AEMeasurable Z P →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : BoundedContinuousFunction G ℝ) (g : BoundedContinuousFunction ((t : T) → F t) ℝ),
          ∫ (x : Ω), (fun ω => f (Z ω) * g fun x => Y x ω) x ∂P =
            (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω => g fun x => Y x ω) x ∂P) →
        ProbabilityTheory.IndepFun Z (fun ω t => Y t ω) P

Defined in

Mathlib.Probability.Independence.BoundedContinuousFunction

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedMeasureTheory.IsFiniteMeasureFinite