seminormAux_le_bound — Mathlib

English

If a nonnegative M bounds all values ∥x∥^k ∥D^n f(x)∥, then f.seminormAux k n ≤ M.

Русский

Если существует M ≥ 0, такое что ∥x∥^k ∥D^n f(x)∥ ≤ M для всех x, тогда f.seminormAux k n ≤ M.

LaTeX

$$$M \\ge 0 \\quad\\wedge\\quad \\forall x, \\|x\\|^k \\cdot \\| \\mathrm{D}^n f(x) \\| \\le M \\quad\\Rightarrow\\quad f.seminormAux_{k,n} \\le M$$$

Lean4

/-- If one controls the norm of every `A x`, then one controls the norm of `A`. -/
theorem seminormAux_le_bound (k n : ℕ) (f : 𝓢(E, F)) {M : ℝ} (hMp : 0 ≤ M)
    (hM : ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ M) : f.seminormAux k n ≤ M :=
  csInf_le (bounds_bddBelow k n f) ⟨hMp, hM⟩

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