Theorems · Theorem · probability

pi_indepFun_pi_of_prod_bcf

∀ {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  {F : T → Type u_5} [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 : (t : T) → TopologicalSpace (F t)]
  [inst_5 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)] [∀ (t : T), HasOuterApproxClosed (F t)]
  {X : (s : S) → Ω → E s} {Y : (t : T) → Ω → F t} [inst_8 : Fintype S] [inst_9 : Fintype T]
  [MeasureTheory.IsFiniteMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ) (g : (t : T) → BoundedContinuousFunction (F t) ℝ),
          ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
            (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P

Defined in

Mathlib.Probability.Independence.BoundedContinuousFunction

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedTopologicalSpaceMeasurableSpaceBorelSpaceHasOuterApproxClosedFintypeFintypeMeasureTheory.IsFiniteMeasure