decay_neg_aux — Mathlib

English

Equality of bounds for f and -f under squared norm bounds.

Русский

Эквивалентность границ для f и -f при квадратированных нормовых ограничениях.

LaTeX

$$$ ||x||^{k} \|D^{n}(-f)(x)\| = ||x||^{k} \|D^{n}f(x)\| $$$

Lean4

theorem decay_neg_aux (k n : ℕ) (f : 𝓢(E, F)) (x : E) :
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-f : E → F) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ := by
  rw [iteratedFDeriv_neg_apply, norm_neg]

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