integrableOn_Ioi_deriv_norm_ofReal_cpow

English

If Re(s) ≤ 0 and t > 0, the derivative of x ↦ ||x^{s}|| is integrable on (t, ∞).

Русский

Если Re(s) ≤ 0 и t > 0, производная функции x ↦ ||x^{s}|| интегрируема на (t, ∞).

LaTeX

$$$\\text{IntegrableOn} \\big( x \\mapsto \\|x^{s}\\| \\big) \\big'(x\\big) (Ioi t)$, \\; t>0, \\; \\Re(s) \\le 0$$$

Lean4

theorem integrableOn_Ioi_deriv_norm_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re ≤ 0) :
    IntegrableOn (deriv fun x : ℝ ↦ ‖(x : ℂ) ^ s‖) (Set.Ioi t) :=
  by
  rw [integrableOn_congr_fun (fun x hx ↦ by rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]) measurableSet_Ioi]
  obtain hs | hs := eq_or_lt_of_le hs
  · simp_rw [hs, zero_mul]
    exact integrableOn_zero
  · replace hs : s.re - 1 < -1 := by rwa [sub_lt_iff_lt_add, neg_add_cancel]
    exact (integrableOn_Ioi_rpow_of_lt hs ht).const_mul s.re

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