fderiv_norm_smul_pos — Mathlib

English

Let E be a real normed space. For any x ∈ E and any t ∈ ℝ with t > 0, the Fréchet derivative of the norm at t x equals the Fréchet derivative of the norm at x; i.e., D‖·‖(t x) = D‖·‖(x).

Русский

Пусть E - евклидово нормированное пространство над ℝ. Для любого x ∈ E и любого t ∈ ℝ с t > 0 производная нормы в точке t x совпадает с производной нормы в точке x; то есть D‖·‖(t x) = D‖·‖(x).

LaTeX

$$$0 < t \\Rightarrow D(\\|\\cdot\\|)_{t x} = D(\\|\\cdot\\|)_x$$$

Lean4

theorem fderiv_norm_smul_pos (ht : 0 < t) : fderiv ℝ (‖·‖) (t • x) = fderiv ℝ (‖·‖) x := by simp [fderiv_norm_smul, ht]

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