English
For differentiable f, the operator norm of the derivative of x ↦ ‖f(x)‖^p is bounded by p‖f(x)‖^{p-1}‖f'(x)‖.
Русский
Для дифференцируемой f норма производной функции x ↦ ‖f(x)‖^p по x удовлетворяет неравенству: ≤ p‖f(x)‖^{p-1}‖f'(x)‖.
LaTeX
$$$\\|f'(x)\\| ≤ p\\|f(x)\\|^{p-1}$ (в соответствующей нормированной форме)$$
Lean4
theorem norm_fderiv_norm_rpow_le {f : F → E} (hf : Differentiable ℝ f) {x : F} {p : ℝ} (hp : 1 < p) :
‖fderiv ℝ (fun x ↦ ‖f x‖ ^ p) x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖ :=
by
rw [hf.fderiv_norm_rpow hp, norm_smul, norm_mul]
simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs, abs_eq_self.mpr <| zero_le_one.trans hp.le,
mul_assoc]
gcongr _ * ?_
refine mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le ..) (by positivity) |>.trans_eq ?_
rw [innerSL_apply_norm, ← mul_assoc, ← Real.rpow_add_one' (by positivity) (by linarith)]
ring_nf
