Theorems · Theorem · probability

ProbabilityTheory.IndepFun.integrable_right_of_integrable_op

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : NormedAddGroup E] [inst_1 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_3 : TopologicalSpace F]
  [inst_4 : ContinuousENorm 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 μ → ¬X =ᵐ[μ] 0 → MeasureTheory.Integrable Y μ

If X and Y are two independent random variables, B X Y is integrable, X is not almost-surely 0 and c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ, then Y 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

2 results in Mathlib

Foundations

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

Assumes

NormedAddGroupMeasurableSpaceOpensMeasurableSpaceTopologicalSpaceContinuousENormMeasurableSpaceOpensMeasurableSpaceTopologicalSpaceContinuousENorm