integrable_rpow_abs_of_integrable_exp_mul

English

If exp((v+t)X) and exp((v−t)X) are integrable with t ≠ 0, then for any p ≥ 0, |X|^p · exp(vX) is integrable.

Русский

Если экспоненты exp((v+t)X) и exp((v−t)X) интегрируемы при t ≠ 0, то для любого p ≥ 0 интегрируемо |X|^p · exp(vX).

LaTeX

$$$\forall p \ge 0: \mathrm{Integrable}\left(|X|^p \exp(v X)\right).$$$

Lean4

/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ p` is
integrable for all nonnegative `p : ℝ`. -/
theorem integrable_rpow_abs_of_integrable_exp_mul (ht : t ≠ 0) (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (-t * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) : Integrable (fun ω ↦ |X ω| ^ p) μ :=
  by
  have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
  · simpa using h
  · simpa using ht_int_pos
  · simpa using ht_int_neg

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