integrableOn_Ioi_deriv_ofReal_cpow

English

For s ∈ ℂ with Re(s) < 0 and t > 0, the derivative of x ↦ x^{s} is integrable on (t, ∞).

Русский

Для s ∈ ℂ с Re(s) < 0 и t > 0 производная по x от x^{s} интегрируема на (t, ∞).

LaTeX

$$$\\text{IntegrableOn} \\big( \\operatorname{deriv} (x \\mapsto x^{s}) \\big) (Ioi t)$, \\; t>0, \\; \\Re(s) < 0$$$

Lean4

theorem integrableOn_Ioi_deriv_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re < 0) :
    IntegrableOn (deriv fun x : ℝ ↦ (x : ℂ) ^ s) (Set.Ioi t) :=
  by
  have h : IntegrableOn (fun x : ℝ ↦ s * x ^ (s - 1)) (Set.Ioi t) :=
    by
    refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _
    rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
  refine h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi
  rw [Complex.deriv_ofReal_cpow_const (ht.trans hx).ne' (fun h ↦ (Complex.zero_re ▸ h ▸ hs).false)]

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