bounds_bddBelow

Mathlib.Analysis.Distribution.SchwartzSpace

URI: https://scilib.ai/kg/mathlib#SchwartzMap.bounds_bddBelow

English

The set of nonnegative bounds is bounded below by 0.

Русский

Множество неотрицательных границ ограничено снизу нулём.

LaTeX

$$$ BddBelow \{ c \mid 0 ≤ c ∧ ∀ x, \|x\|^{k} \|iteratedFDeriv^n f x\| ≤ c \} $$$

Lean4

theorem bounds_bddBelow (k n : ℕ) (f : 𝓢(E, F)) : BddBelow {c | 0 ≤ c ∧ ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ c} :=
  ⟨0, fun _ ⟨hn, _⟩ => hn⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru