Theorems · Theorem · probability

ProbabilityTheory.integrable_exp_mul_of_abs_le

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

If ω ↦ exp (u * X ω) is integrable at u and -u, then it is integrable on [-u, u].

Defined in

Mathlib.Probability.Moments.IntegrableExpMul

Cited by

0 results in Mathlib

Foundations

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