integrable_pow_abs_mul_exp_add_of_integrable_exp_mul

English

If exp((v+t)X) and exp((v−t)X) are integrable, then for any x with 0 ≤ x < |t| and any n ∈ ℕ, the quantity |X|^n · exp(vX) is integrable.

Русский

Если экспонтненты эксп((v+t)X) и эксп((v−t)X) интегрируемы, то при любом x с 0 ≤ x < |t| и любом n ∈ ℕ интегрируемо |X|^n · exp(vX).

LaTeX

$$$\forall x \in [0, |t|), \forall n \in \mathbb{N}: \mathrm{Integrable}\left(|X|^n \exp(v X)\right).$$$

Lean4

/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for any `n : ℕ` and any `x ∈ [0, |t|)`,
`|X| ^ n * exp (v * X + x * |X|)` is integrable. -/
theorem integrable_pow_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|) (n : ℕ) : Integrable (fun a ↦ |X a| ^ n * exp (v * X a + x * |X a|)) μ :=
  by
  convert integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul h_int_pos h_int_neg h_nonneg hx n.cast_nonneg
  simp

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