English
The property of temperate growth is stable under standard SchwartzMap operations; in particular, every SchwartzMap has temperate growth.
Русский
Свойство темперированного роста сохраняется под стандартными операциями SchwartzMap; в частности, вся SchwartzMap имеет темперированный рост.
LaTeX
$$$\\forall f\\in \\mathcal{S}(E,F): fHasTemperateGrowth$.$$
Lean4
/-- A smooth compactly supported function is a Schwartz function. -/
@[simps]
def _root_.HasCompactSupport.toSchwartzMap {f : E → F} (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ ∞ f) : 𝓢(E, F)
where
toFun := f
smooth' := h₂
decay' k
n := by
set g := fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖
have hg₁ : Continuous g := by
apply Continuous.mul (by fun_prop)
exact (h₂.of_le (right_eq_inf.mp rfl)).continuous_iteratedFDeriv'.norm
have hg₂ : HasCompactSupport g := (h₁.iteratedFDeriv _).norm.mul_left
obtain ⟨x₀, hx₀⟩ := hg₁.exists_forall_ge_of_hasCompactSupport hg₂
exact ⟨g x₀, hx₀⟩
