Theorems · Theorem · probability

ProbabilityTheory.IndepFun.integrable_op

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E]
  [inst_4 : TopologicalSpace F] [inst_5 : ContinuousENorm F] [inst_6 : MeasurableSpace F] [OpensMeasurableSpace F]
  [inst_8 : TopologicalSpace G] [inst_9 : ContinuousENorm G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ →
      MeasureTheory.Integrable Y μ →
        ∀ (B : E → F → G),
          Continuous (Function.uncurry B) →
            ∀ (C : NNReal),
              (∀ (x : E) (y : F), ‖B x y‖ₑ ≤ ↑C * ‖x‖ₑ * ‖y‖ₑ) → MeasureTheory.Integrable (fun ω => B (X ω) (Y ω)) μ

If X and Y are two independent and integrable random variables, and B is a function of two variables such that ‖B x y‖ₑ ≤ C * ‖x‖ₑ * ‖y‖ₑ, then B X Y is integrable. This is useful in particular if B is a continuous bilinear map.

Defined in

Mathlib.Probability.Independence.Integration

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENormMeasurableSpaceOpensMeasurableSpaceTopologicalSpaceContinuousENormMeasurableSpaceOpensMeasurableSpaceTopologicalSpaceContinuousENorm