integrable_pow_abs_of_integrable_exp_mul

English

If 0 lies in the interior of the integrableExponentialSet for X, then for every p ≥ 0, |X|^p is integrable.

Русский

Если 0 лежит во внутренности интегрируемого экспонентного множества для X, то для каждого p ≥ 0 |X|^p интегрируемо.

LaTeX

$$$\text{If } 0 \in \operatorname{interior}(\text{integrableExpSet}(X, \mu)) \text{ then } \forall p \ge 0: \mathrm{Integrable}(|X|^p).$$$

Lean4

/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ n` is
integrable for all `n : ℕ`. That is, all moments of `X` are finite. -/
theorem integrable_pow_abs_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_abs_of_integrable_exp_mul ht ht_int_pos ht_int_neg (by positivity : 0 ≤ (n : ℝ)) with ω
  simp

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