English
If 0 lies in the interior of integrableExpSet X μ, then for every natural n, |X|^n is integrable.
Русский
Если 0 лежит во внутренности множества интегрируемости экспоненты, то для каждого натурального n |X|^n интегрируемо.
LaTeX
$$$\text{If } 0 \in \operatorname{int}(\text{integrableExpSet}(X,\mu)) \text{ then } \forall n \in \mathbb{N}: \mathrm{Integrable}(|X|^n).$$$
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_abs_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_abs_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)
