Theorems · Theorem · probability

ProbabilityTheory.IndepFun.integral_bilin_comp_comp

∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3}
  {𝓨 : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst_1 : MeasurableSpace 𝓧] [inst_2 : MeasurableSpace 𝓨]
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 E] [CompleteSpace E]
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedSpace 𝕜 F] [CompleteSpace F]
  [inst_11 : NormedAddCommGroup G] [inst_12 : NormedSpace ℝ G] [inst_13 : NormedSpace 𝕜 G] [CompleteSpace G] {X : Ω → 𝓧}
  {Y : Ω → 𝓨} {f : 𝓧 → E} {g : 𝓨 → F},
  ProbabilityTheory.IndepFun X Y μ →
    AEMeasurable X μ →
      AEMeasurable Y μ →
        MeasureTheory.Integrable f (MeasureTheory.Measure.map X μ) →
          MeasureTheory.Integrable g (MeasureTheory.Measure.map Y μ) →
            ∀ (B : E →L[𝕜] F →L[𝕜] G),
              ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

If X and Y are independent random variables such that f(X) and g(Y) are integrable and B is a continuous bilinear map, then ∫ ω, B (f (X ω)) (g (Y ω)) ∂μ = B (∫ ω, f (X ω) ∂μ) (∫ ω, g (Y ω) ∂μ).

Defined in

Mathlib.Probability.Independence.Integration

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeMeasurableSpaceMeasurableSpaceNormedAddCommGroupNormedSpaceNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceNormedSpaceCompleteSpace