English
If exp((v+t)X) and exp((v−t)X) are integrable, then for all nonnegative x with 0 ≤ x < |t|, and for every p ≥ 0, the function |X|^p · exp(vX + x|X|) is integrable.
Русский
Если exp((v+t)X) и exp((v−t)X) интегрируемы, то для всех неотрицательных x с 0 ≤ x < |t| и для каждого p ≥ 0 функция |X|^p · exp(vX + x|X|) интегрируема.
LaTeX
$$$\forall x \in [0, |t|), \forall p \in \mathbb{R}_{\ge 0}: \mathrm{Integrable}\left(|X|^p \exp(v X + x |X|)\right).$$$
Lean4
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for nonnegative `p : ℝ` and any `x ∈ [0, |t|)`,
`|X| ^ p * exp (v * X + x * |X|)` is integrable. -/
theorem integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul {x : ℝ}
(h_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ) (h_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ)
(h_nonneg : 0 ≤ x) (hx : x < |t|) {p : ℝ} (hp : 0 ≤ p) :
Integrable (fun a ↦ |X a| ^ p * exp (v * X a + x * |X a|)) μ :=
by
have ht : t ≠ 0 := by
suffices |t| ≠ 0 by simpa
exact (h_nonneg.trans_lt hx).ne'
have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ h_int_pos h_int_neg
swap; · rw [← sub_ne_zero]; simp [ht]
rw [← integrable_norm_iff]
swap; · fun_prop
simp only [norm_mul, norm_eq_abs, abs_exp]
have h_le a : |X a| ^ p * exp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|) :=
by
simp_rw [exp_add, mul_comm (exp (v * X a)), ← mul_assoc]
gcongr ?_ * _
have : |t| = |t| - x + x := by simp
nth_rw 2 [this]
rw [add_mul, exp_add, ← mul_assoc]
gcongr ?_ * _
convert rpow_abs_le_mul_exp_abs (X a) hp (t := |t| - x) _ using 4
· nth_rw 2 [abs_of_nonneg]
simp [hx.le]
· nth_rw 2 [abs_of_nonneg]
simp [hx.le]
· rw [sub_ne_zero]
exact hx.ne'
refine
Integrable.mono (g := fun a ↦ (p / (|t| - x)) ^ p * exp (v * X a + |t| * |X a|)) ?_ ?_ <| ae_of_all _ fun ω ↦ ?_
· refine Integrable.const_mul ?_ _
simp_rw [add_comm (v * X _)]
exact integrable_exp_abs_mul_abs_add h_int_pos h_int_neg
· fun_prop
· simp only [norm_mul, norm_eq_abs, abs_exp]
simp_rw [abs_rpow_of_nonneg (abs_nonneg _), abs_abs]
refine (h_le ω).trans_eq ?_
congr
symm
simp only [abs_eq_self]
exact rpow_nonneg (div_nonneg hp (sub_nonneg_of_le hx.le)) _
