English
For a real inner product space and p > 1, the derivative of x ↦ ‖x‖^p at x is given by p‖x‖^(p−2) x.
Русский
Для вещественного пространства с векторным скалярным произведением и p > 1 производная функции x ↦ ‖x‖^p по x равна p‖x‖^(p−2) x.
LaTeX
$$$\\text{HasDerivAt}(x \\mapsto \\|x\\|^p, p\\|x\\|^{p-2}x, x)$$$
Lean4
theorem hasFDerivAt_norm_rpow (x : E) {p : ℝ} (hp : 1 < p) :
HasFDerivAt (fun x : E ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • innerSL ℝ x) x :=
by
by_cases hx : x = 0
· simp only [hx, norm_zero, map_zero, smul_zero]
have h2p : 0 < p - 1 := sub_pos.mpr hp
rw [HasFDerivAt, hasFDerivAtFilter_iff_isLittleO]
calc
(fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0) = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
_ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
ext x
rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
ring_nf
_ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) :=
by
refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
convert continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
simp [h2p.ne']
_ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
· apply HasStrictFDerivAt.hasFDerivAt
convert (hasStrictFDerivAt_norm_sq x).rpow_const (p := p / 2) (by simp [hx]) using 0
simp_rw [← Real.rpow_natCast_mul (norm_nonneg _), ← Nat.cast_smul_eq_nsmul ℝ, smul_smul]
ring_nf
