English
A smooth compactly supported function is a Schwartz map; the construction records decay bounds.
Русский
Плавная компактно поддержанная функция — это отображение Шварца; конструктор фиксирует декей Bound.
LaTeX
$$$HasCompactSupport\\toSchwartzMap\\; (h_1,h_2):\\; 𝓢(E,F)$.$$
Lean4
/-- Create a semilinear map between Schwartz spaces.
Note: This is a helper definition for `mkCLM`. -/
def mkLM (A : 𝓢(D, E) → F → G) (hadd : ∀ (f g : 𝓢(D, E)) (x), A (f + g) x = A f x + A g x)
(hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)) (x), A (a • f) x = σ a • A f x) (hsmooth : ∀ f : 𝓢(D, E), ContDiff ℝ ∞ (A f))
(hbound :
∀ n : ℕ × ℕ,
∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
0 ≤ C ∧
∀ (f : 𝓢(D, E)) (x : F),
‖x‖ ^ n.fst * ‖iteratedFDeriv ℝ n.snd (A f) x‖ ≤ C * s.sup (schwartzSeminormFamily 𝕜 D E) f) :
𝓢(D, E) →ₛₗ[σ] 𝓢(F, G)
where
toFun
f :=
{ toFun := A f
smooth' := hsmooth f
decay' := by
intro k n
rcases hbound ⟨k, n⟩ with ⟨s, C, _, h⟩
exact ⟨C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f, h f⟩ }
map_add' f g := ext (hadd f g)
map_smul' a f := ext (hsmul a f)
