English
For a complex exponent c and positive t, the derivative at t of the real-valued function t ↦ |t^c| equals Re(c) · t^{Re(c) - 1}. In particular, for t > 0, d/dt |t^c| = Re(c) t^{Re(c)-1}.
Русский
Для комплексного показателя c и положительного t производная функции t ↦ |t^c| равна Re(c) · t^{Re(c)−1}. В частности, при t > 0: d/dt |t^c| = Re(c) t^{Re(c)−1}.
LaTeX
$$$\\displaystyle \\frac{d}{dt}\\bigl|t^{c}\\bigr| = \\Re(c) \\cdot t^{\\Re(c)-1} \\quad (t>0)$$$
Lean4
theorem deriv_norm_ofReal_cpow (c : ℂ) {t : ℝ} (ht : 0 < t) :
(deriv fun x : ℝ ↦ ‖(x : ℂ) ^ c‖) t = c.re * t ^ (c.re - 1) :=
by
rw [EventuallyEq.deriv_eq (f := fun x ↦ x ^ c.re)]
· rw [Real.deriv_rpow_const (Or.inl ht.ne')]
· filter_upwards [eventually_gt_nhds ht] with x hx
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx]
