English
An alternative formulation expresses the differentiability of the real-variable cpow in terms of real-domain derivatives; in particular, for x ≠ 0 and r ≠ -1 the real-variable cpow is differentiable with a specified derivative formula.
Русский
Альтернативная формулировка выражает дифференцируемость cpow при переменной по вещественной оси; в частности, при x ≠ 0 и r ≠ -1 функция x ↦ x^{r+1}/(r+1) имеет производную x^{r} и т. д.
LaTeX
$$$\\text{For real }x\\neq 0\\text{ and }r\\neq -1,\\ x\\mapsto x^{r} \\text{ is differentiable with derivative } r x^{r-1}. $$$
Lean4
/-- Although `fun x => x ^ r` for fixed `r` is *not* complex-differentiable along the negative real
line, it is still real-differentiable, and the derivative is what one would formally expect.
See `hasDerivAt_ofReal_cpow_const` for an alternate formulation. -/
theorem hasDerivAt_ofReal_cpow_const' {x : ℝ} (hx : x ≠ 0) {r : ℂ} (hr : r ≠ -1) :
HasDerivAt (fun y : ℝ => (y : ℂ) ^ (r + 1) / (r + 1)) (x ^ r) x :=
by
rw [Ne, ← add_eq_zero_iff_eq_neg, ← Ne] at hr
rcases lt_or_gt_of_ne hx.symm with (hx | hx)
· -- easy case : `0 < x`
apply HasDerivAt.comp_ofReal (e := fun y => (y : ℂ) ^ (r + 1) / (r + 1))
convert HasDerivAt.div_const (𝕜 := ℂ) ?_ (r + 1) using 1
· exact (mul_div_cancel_right₀ _ hr).symm
· convert HasDerivAt.cpow_const ?_ ?_ using 1
· rw [add_sub_cancel_right, mul_comm]; exact (mul_one _).symm
· exact hasDerivAt_id (x : ℂ)
· simp [hx]
· -- harder case : `x < 0`
have : ∀ᶠ y : ℝ in 𝓝 x, (y : ℂ) ^ (r + 1) / (r + 1) = (-y : ℂ) ^ (r + 1) * exp (π * I * (r + 1)) / (r + 1) :=
by
refine Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_
rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
refine HasDerivAt.congr_of_eventuallyEq ?_ this
rw [ofReal_cpow_of_nonpos (le_of_lt hx)]
suffices
HasDerivAt (fun y : ℝ => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
by
convert this.div_const (r + 1) using 1
conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]
rw [mul_add ((π : ℂ) * _), mul_one, exp_add, exp_pi_mul_I, mul_comm (_ : ℂ) (-1 : ℂ), neg_one_mul]
simp_rw [mul_neg, ← neg_mul, ← ofReal_neg]
suffices HasDerivAt (fun y : ℝ => (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by
convert this.neg.mul_const _ using 1; ring
suffices HasDerivAt (fun y : ℝ => (y : ℂ) ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
by
convert @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
rw [real_smul, ofReal_neg 1, ofReal_one]; ring
suffices HasDerivAt (fun y : ℂ => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x) by exact this.comp_ofReal
conv in ↑_ ^ _ => rw [(by ring : r = r + 1 - 1)]
convert HasDerivAt.cpow_const ?_ ?_ using 1
· rw [add_sub_cancel_right, add_sub_cancel_right]; exact (mul_one _).symm
· exact hasDerivAt_id ((-x : ℝ) : ℂ)
· simp [hx]
