English
A family of seminorms on the Schwartz space is defined, indexed by natural numbers (k,n), giving the best constants in the defining inequalities for each pair.
Русский
Семинормы на Schwartz-пространстве задаются семейством, индексируемым парами (k,n), отвечая за наилучшие константы в неравенствах определения для каждой пары.
LaTeX
$$$\mathrm{seminorm}(k,n):= \mathrm{Seminorm}.ofSMulLE(\mathrm{SchwartzMap.seminormAux}(k,n), \mathrm{seminormAuxZero}(k,n), \mathrm{seminormAuxAddLe}(k,n), \mathrm{seminormAuxSmulLe}(k,n))$$$
Lean4
/-- The seminorms of the Schwartz space given by the best constants in the definition of
`𝓢(E, F)`. -/
protected def seminorm (k n : ℕ) : Seminorm 𝕜 𝓢(E, F) :=
Seminorm.ofSMulLE (SchwartzMap.seminormAux k n) (seminormAux_zero k n) (seminormAux_add_le k n)
(seminormAux_smul_le k n)
