Theorems · Theorem · probability

ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul

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

If exp ((v + t) * X) and exp ((v - t) * X) are integrable, then for all nonnegative p : ℝ, X ^ p * exp (v * X) is integrable.

Defined in

Mathlib.Probability.Moments.IntegrableExpMul

Cited by

3 results in Mathlib

Foundations

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