Theorems · Theorem · probability

ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet

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

If v belongs to the interior of the interval integrableExpSet X μ, then X ^ p * exp (v * X) is integrable for all nonnegative p : ℝ.

Defined in

Mathlib.Probability.Moments.IntegrableExpMul

Cited by

2 results in Mathlib

Foundations

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