integrableOn_Ioi_norm_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$, $t>0$$$

Lean4

theorem integrableOn_Ioi_norm_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) :
    IntegrableOn (fun x : ℝ ↦ ‖(x : ℂ) ^ s‖) (Ioi t) ↔ s.re < -1 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_norm_cpow_of_lt h ht⟩
  refine (integrableOn_Ioi_rpow_iff ht).mp <| h.congr_fun (fun a ha ↦ ?_) measurableSet_Ioi
  rw [Complex.norm_cpow_eq_rpow_re_of_pos (ht.trans ha)]

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