integrable_rpow_mul_exp_of_mem_interior_integrableExpSet

English

If 0 lies in interior of integrableExpSet, then for every p≥0, |X|^p · exp(v X) is integrable.

Русский

Если 0 лежит во внутренности integrableExpSet, то для любого p≥0 |X|^p · exp(vX) интегрируемо.

LaTeX

$$$\forall p \ge 0: \mathrm{Integrable}(|X|^p \exp(v X)).$$$

Lean4

/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ p * exp (v * X)` is integrable for all nonnegative `p : ℝ`. -/
theorem integrable_rpow_mul_exp_of_mem_interior_integrableExpSet (hv : v ∈ interior (integrableExpSet X μ)) {p : ℝ}
    (hp : 0 ≤ p) : Integrable (fun ω ↦ X ω ^ p * exp (v * X ω)) μ :=
  by
  rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv
  obtain ⟨l, u, hvlu, h_subset⟩ := hv
  have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
  refine integrable_rpow_mul_exp_of_integrable_exp_mul (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
  · positivity
  · exact h_subset (add_half_inf_sub_mem_Ioo hvlu)
  · exact h_subset (sub_half_inf_sub_mem_Ioo hvlu)

Похожие утверждения