Theorems · Theorem · probability

ProbabilityTheory.IndepFun.integrable_left_of_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 : NormedAddGroup F] [inst_5 : MeasurableSpace F] [OpensMeasurableSpace F] [inst_7 : TopologicalSpace G]
  [inst_8 : ContinuousENorm G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    ∀ (B : E → F → G) (c : NNReal),
      c ≠ 0 →
        (∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ) →
          MeasureTheory.Integrable (fun ω => B (X ω) (Y ω)) μ →
            MeasureTheory.AEStronglyMeasurable X μ →
              MeasureTheory.AEStronglyMeasurable Y μ → ¬Y =ᵐ[μ] 0 → MeasureTheory.Integrable X μ

If X and Y are two independent random variables, B X Y is integrable, Y is not almost-surely 0 and c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ, then X is integrable. This is useful for the case where B is scalar multiplication, as it will allow to drop integrability hypotheses.

Defined in

Mathlib.Probability.Independence.Integration

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENormMeasurableSpaceOpensMeasurableSpaceNormedAddGroupMeasurableSpaceOpensMeasurableSpaceTopologicalSpaceContinuousENorm