nnnorm_fderiv_norm_rpow_le — Mathlib

English

The nonnegative norm of the derivative of a norm^p function in NNReal setting is bounded by a product formula with p, norm, and derivative norms.

Русский

Нормированная по NNReal производная функции ‖f(x)‖^p имеет верхнюю грань, выражаемую через p, норму и норму производной.

LaTeX

$$$\\text{nnnorm}(f') ≤ p\\,\\|f(x)\\|^{p-1}\\cdot \\text{nnnorm}(f')$$$

Lean4

theorem nnnorm_fderiv_norm_rpow_le {f : F → E} (hf : Differentiable ℝ f) {x : F} {p : ℝ≥0} (hp : 1 < p) :
    ‖fderiv ℝ (fun x ↦ ‖f x‖ ^ (p : ℝ)) x‖₊ ≤ p * ‖f x‖₊ ^ ((p : ℝ) - 1) * ‖fderiv ℝ f x‖₊ :=
  norm_fderiv_norm_rpow_le hf hp

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