English
Let E be a real normed inner product space and p > 1. The map x ↦ ||x||^p is continuously differentiable of order 1 on E.
Русский
Пусть E — нормированное пространство с тензорной скалярной площадкой над ℝ, и p > 1. Отображение x ↦ ||x||^p непрерывно дифференцируемо первого порядка по x.
LaTeX
$$$\forall p>1,\ ContDiff_{\mathbb{R}}^{1}(x \mapsto \|x\|^{p}).$$$
Lean4
theorem contDiff_norm_rpow {p : ℝ} (hp : 1 < p) : ContDiff ℝ 1 (fun x : E ↦ ‖x‖ ^ p) :=
by
rw [contDiff_one_iff_fderiv]
refine ⟨fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt, ?_⟩
simp_rw [continuous_iff_continuousAt]
intro x
by_cases hx : x = 0
· simp_rw [hx, ContinuousAt, fderiv_norm_rpow (0 : E) hp, norm_zero, map_zero, smul_zero]
rw [tendsto_zero_iff_norm_tendsto_zero]
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le (tendsto_const_nhds) ?_ (fun _ ↦ norm_nonneg _)
(fun _ ↦ norm_fderiv_norm_id_rpow _ hp |>.le)
suffices ContinuousAt (fun x : E ↦ p * ‖x‖ ^ (p - 1)) 0 by simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this
fun_prop (discharger := simp [hp.le])
· simp_rw [funext fun x ↦ fderiv_norm_rpow (E := E) (x := x) hp]
fun_prop (discharger := simp [hx])
