integrable_pow_of_integrable_exp_mul

English

If exp((v+t)X) and exp((v−t)X) are integrable, then for any n ∈ ℕ, |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 (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ X ω ^ n` is
integrable for all `n : ℕ`. -/
theorem integrable_pow_of_integrable_exp_mul (ht : t ≠ 0) (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (-t * X ω)) μ) (n : ℕ) : Integrable (fun ω ↦ X ω ^ n) μ :=
  by
  convert integrable_rpow_of_integrable_exp_mul ht ht_int_pos ht_int_neg (by positivity : 0 ≤ (n : ℝ)) with ω
  simp

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