English
If exp((v+t)X) and exp((v−t)X) are integrable, then for every nonnegative p, |X|^p · exp(vX) is integrable.
Русский
Если экспоненты эксп((v+t)X) и эксп((v−t)X) интегрируемы, то для любого p≥0 интегрируема |X|^p · exp(vX).
LaTeX
$$$\forall p \ge 0: \mathrm{Integrable}\left(|X|^p \exp(v X)\right).$$$
Lean4
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all nonnegative `p : ℝ`,
`X ^ p * exp (v * X)` is integrable. -/
theorem integrable_rpow_mul_exp_of_integrable_exp_mul (ht : t ≠ 0)
(ht_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ) (ht_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ)
{p : ℝ} (hp : 0 ≤ p) : Integrable (fun ω ↦ X ω ^ p * exp (v * X ω)) μ :=
by
have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ ht_int_pos ht_int_neg
swap; · rw [← sub_ne_zero]; simp [ht]
rw [← integrable_norm_iff]
· simp_rw [norm_eq_abs, abs_mul, abs_exp]
have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg hp
refine h.mono' ?_ ?_
· fun_prop
· refine ae_of_all _ fun ω ↦ ?_
simp only [norm_mul, norm_eq_abs, abs_abs, abs_exp]
gcongr
exact abs_rpow_le_abs_rpow _ _
· fun_prop
