differentiableAt_norm_of_smul — Mathlib

English

For t ≠ 0, ContDiffAt of the norm at t x is equivalent to ContDiffAt at x; i.e., contDiffAt_norm_smul_iff holds.

Русский

При t ≠ 0 ContDiffAt нормы в t x эквивалентна ContDiffAt в x.

LaTeX

$$$\\text{ContDiffAt}_{\\mathbb{R}}(n)(\\|\\cdot\\|)(t x) \\\\iff \\\\ \\text{ContDiffAt}_{\\mathbb{R}}(n)(\\|\\cdot\\|)(x) \\quad (t \\neq 0)$$$

Lean4

theorem differentiableAt_norm_of_smul (h : DifferentiableAt ℝ (‖·‖) (t • x)) : DifferentiableAt ℝ (‖·‖) x :=
  by
  obtain rfl | ht := eq_or_ne t 0
  · by_cases hE : Nontrivial E
    · rw [zero_smul] at h
      exact not_differentiableAt_norm_zero E h |>.elim
    · push_neg at hE
      exact (hasFDerivAt_of_subsingleton _ _).differentiableAt
  · exact differentiableAt_norm_smul ht |>.2 h

Похожие утверждения