decay_add_le_aux — Mathlib

English

An auxiliary inequality bounding the sum of two derivatives by the derivative of the sum.

Русский

Вспомогательное неравенство, ограничивающее сумму производных через производную суммы.

LaTeX

$$$ \|x\|^{k} \|D^{n}(f+g)(x)\| ≤ \|x\|^{k} \|D^{n}f(x)\| + \|x\|^{k} \|D^{n}g(x)\| $$$

Lean4

theorem decay_add_le_aux (k n : ℕ) (f g : 𝓢(E, F)) (x : E) :
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n ((f : E → F) + (g : E → F)) x‖ ≤
      ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n g x‖ :=
  by
  rw [← mul_add]
  gcongr _ * ?_
  rw [iteratedFDeriv_add_apply (f.smooth _).contDiffAt (g.smooth _).contDiffAt]
  exact norm_add_le _ _

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