integrable_rpow_abs_mul_exp_of_integrable_exp_mul

English

If t ≠ 0 and exp((v+t)X) and exp((v−t)X) are integrable, then for every nonnegative p, the expression |X|^p · exp(vX) is integrable.

Русский

Если t ≠ 0 и exp((v+t)X) и exp((v−t)X) интегрируемы, то для любого неотрицательного p интегрируемо |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 nonnegative `p : ℝ`, `|X| ^ p * exp (v * X)` is integrable. -/
theorem integrable_rpow_abs_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
  convert integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul ht_int_pos ht_int_neg le_rfl _ hp using 4
  · simp
  · simp [ht]

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