Theorems · Theorem · probability

ProbabilityTheory.integrable_rpow_of_integrable_exp_mul

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ →
        ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => X ω ^ p) μ

If ω ↦ exp (t * X ω) is integrable at t and -t for t ≠ 0, then ω ↦ X ω ^ p is integrable for all nonnegative p : ℝ.

Defined in

Mathlib.Probability.Moments.IntegrableExpMul

Cited by

1 results in Mathlib

Foundations

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