integrableOn_Ioi_cpow_of_lt — Mathlib

English

If a ∈ ℂ with Re(a) < -1 and c > 0, then ∫_{c}^{∞} x^{a} dx is finite.

Русский

Если a ∈ ℂ, Re(a) < -1 и c > 0, то ∫_{c}^{∞} x^{a} dx конечен.

LaTeX

$$$\\int_{c}^{\\infty} x^{a} \\, dx < \\infty$$$

Lean4

theorem integrableOn_Ioi_cpow_of_lt {a : ℂ} (ha : a.re < -1) {c : ℝ} (hc : 0 < c) :
    IntegrableOn (fun t : ℝ => (t : ℂ) ^ a) (Ioi c) :=
  by
  refine (integrable_norm_iff ?_).mp <| integrableOn_Ioi_norm_cpow_of_lt ha hc
  refine ContinuousOn.aestronglyMeasurable (fun t ht ↦ ?_) measurableSet_Ioi
  exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt

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