instNeg — Mathlib

English

There is a negation operation on Schwartz maps that preserves smoothness and decay bounds.

Русский

Существование операции отрицания на SchwartzMap сохраняет гладкость и границы распада.

LaTeX

$$Neg f ∈ 𝓢(E,F) with decay' bounds: ∀ k,n, f.seminormAux k n ≤ f.seminormAux k n$$

Lean4

instance instNeg : Neg 𝓢(E, F) :=
  ⟨fun f =>
    ⟨-f, (f.smooth _).neg, fun k n =>
      ⟨f.seminormAux k n, fun x => (decay_neg_aux k n f x).le.trans (f.le_seminormAux k n x)⟩⟩⟩

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