Theorems · Theorem · probability

ProbabilityTheory.IndepFun.integral_bilin

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E] [BorelSpace E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [CompleteSpace F] [inst_8 : MeasurableSpace F]
  [BorelSpace F] [inst_10 : NormedAddCommGroup G] [inst_11 : NormedSpace ℝ G] [CompleteSpace G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ →
      MeasureTheory.Integrable Y μ →
        ∀ (B : E →L[ℝ] F →L[ℝ] G), ∫ (ω : Ω), (B (X ω)) (Y ω) ∂μ = (B (∫ (x : Ω), X x ∂μ)) (∫ (x : Ω), Y x ∂μ)

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

Defined in

Mathlib.Probability.Independence.Integration

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceCompleteSpace