integrable_pow_mul_exp_of_integrable_exp_mul

English

If exp((v+t)X) and exp((v−t)X) are integrable, then for all 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 ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all `n : ℕ`,
`X ^ n * exp (v * X)` is integrable. -/
theorem integrable_pow_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_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg (by positivity : 0 ≤ (n : ℝ)) with ω
  simp

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