integrable_pow_abs_mul_exp_of_integrable_exp_mul

English

If exp((v+t)X) and exp((v−t)X) are integrable, then for every n ∈ ℕ, the product |X|^n · exp(vX) is integrable.

Русский

Если экспоненты exp((v+t)X) и exp((v−t)X) интегрируемы, то для каждого n ∈ ℕ интегрируема |X|^n · exp(vX).

LaTeX

$$$\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 all `n : ℕ`,
`|X| ^ n * exp (v * X)` is integrable. -/
theorem integrable_pow_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 ω)) μ)
    (n : ℕ) : Integrable (fun ω ↦ |X ω| ^ n * exp (v * X ω)) μ :=
  by
  convert integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg (by positivity : 0 ≤ (n : ℝ)) with
    ω
  simp

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