Auxiliary lemmas for SchwartzMap

This file collects small lemmas and constructors for SchwartzMap that are missing from Mathlib, in particular a constructor SchwartzMap.mkOfCocompact which builds a Schwartz map from a decay condition that only needs to hold eventually at infinity (cocompactly), rather than for all x.

@[simp]

theorem SchwartzMap.mk_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {smooth : ContDiff ℝ (↑⊤) f} {decay : ∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C} (x : E) : { toFun := f, smooth' := smooth, decay' := decay } x = f x

@[simp]

theorem natCast_le_coe_top {n : ℕ} : ↑n ≤ ↑⊤

def SchwartzMap.mkOfCocompact {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (smooth : ContDiff ℝ (↑⊤) f) (decay : ∀ (k n : ℕ), ∃ (C : ℝ), ∀ᶠ (x : E) in Filter.cocompact E, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C) : SchwartzMap E F

Construct a SchwartzMap from a smooth function f whose Schwartz decay bounds only need to hold eventually at infinity (i.e. cocompactly), rather than for every x. This relaxes the hypothesis of the anonymous-constructor form ⟨f, smooth, decay⟩, since on a bounded region a continuous function is automatically bounded.

Equations

• SchwartzMap.mkOfCocompact f smooth decay = { toFun := f, smooth' := smooth, decay' := ⋯ }

@[simp]

theorem SchwartzMap.mkOfCocompact_toFun {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (smooth : ContDiff ℝ (↑⊤) f) (decay : ∀ (k n : ℕ), ∃ (C : ℝ), ∀ᶠ (x : E) in Filter.cocompact E, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C) (a✝ : E) : (mkOfCocompact f smooth decay) a✝ = f a✝