English
If E is a nontrivial normed space and a norm is differentiable at x, then the operator norm of the derivative of the norm at x is 1; i.e., ||D‖·‖(x)|| = 1.
Русский
Пусть E не нулево по смыслу нормы, а функция нормы дифференцируема в точке x; тогда операторная норма производной нормы в точке x равна единице; то есть ||D‖·‖(x)|| = 1.
LaTeX
$$$\\|D(\\|\\cdot\\|)_x\\| = 1$$$
Lean4
theorem norm_fderiv_norm [Nontrivial E] (h : DifferentiableAt ℝ (‖·‖) x) : ‖fderiv ℝ (‖·‖) x‖ = 1 :=
by
have : x ≠ 0 := fun hx ↦ not_differentiableAt_norm_zero E (hx ▸ h)
refine le_antisymm (NNReal.coe_one ▸ norm_fderiv_le_of_lipschitz ℝ lipschitzWith_one_norm) ?_
apply le_of_mul_le_mul_right _ (norm_pos_iff.2 this)
calc
1 * ‖x‖ = fderiv ℝ (‖·‖) x x := by rw [one_mul, h.fderiv_norm_self]
_ ≤ ‖fderiv ℝ (‖·‖) x x‖ := (le_norm_self _)
_ ≤ ‖fderiv ℝ (‖·‖) x‖ * ‖x‖ := le_opNorm _ _
