integrableOn_Ioi_cpow_iff — Mathlib

English

For t > 0, ∫_{t}^{∞} x^{s} dx converges iff Re(s) < -1.

Русский

Для t>0 интегрируемость ∫_{t}^{∞} x^{s} dx эквивалентна Re(s) < -1.

LaTeX

$$$\\text{IntegrableOn} (x \\mapsto x^{s}) (Ioi t) \\iff \\Re(s) < -1$$$

Lean4

theorem integrableOn_Ioi_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) :
    IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioi t) ↔ s.re < -1 :=
  ⟨fun h ↦ (integrableOn_Ioi_norm_cpow_iff ht).mp h.norm, fun h ↦ integrableOn_Ioi_cpow_of_lt h ht⟩

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