integrableOn_Ioo_cpow_iff — Mathlib

English

The complex power x^s is integrable on the interval (0,t) iff Re(s) > -1.

Русский

Функция x^s интегрируема на интервале (0,t) тогда и только тогда, когда Re(s) > -1.

LaTeX

$$$\forall s\in\mathbb{C}, t>0:\; \int_{0}^{t} x^{s} dx < \infty \iff \Re(s) > -1$$$

Lean4

/-- The complex power function `x ↦ x^s` is integrable on `(0, t)` iff `-1 < s.re`. -/
theorem integrableOn_Ioo_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) :
    IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioo (0 : ℝ) t) ↔ -1 < s.re :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  swap
  · rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
    exact intervalIntegrable_cpow' h (a := 0) (b := t)
  have B : IntegrableOn (fun a ↦ a ^ s.re) (Ioo 0 t) :=
    by
    apply (integrableOn_congr_fun _ measurableSet_Ioo).1 h.norm
    intro a ha
    simp [Complex.norm_cpow_eq_rpow_re_of_pos ha.1]
  rwa [integrableOn_Ioo_rpow_iff ht] at B

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