bounds_nonempty — Mathlib

English

There exists a bound in the set of nonnegative constants bounding ∥x∥^k ∥iteratedFDeriv^n f x∥.

Русский

Существует граница в множeстве неотрицательных констант, ограничивающих ∥x∥^k ∥iteratedFDeriv^n f x∥.

LaTeX

$$$ ∃ c ∈ {c ∈ \mathbb{R} \mid 0 ≤ c ∧ ∀ x, \|x\|^{k} \|iteratedFDeriv^n f x\| ≤ c} $$$

Lean4

theorem bounds_nonempty (k n : ℕ) (f : 𝓢(E, F)) :
    ∃ c : ℝ, c ∈ {c : ℝ | 0 ≤ c ∧ ∀ x : E, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ c} :=
  let ⟨M, hMp, hMb⟩ := f.decay k n
  ⟨M, le_of_lt hMp, hMb⟩

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