noncomputable def SchwartzMap.bumpSeq {E : Type u_1} [NormedAddCommGroup E] (m : ℕ) : ContDiffBump 0

A sequence of smooth bump functions χ_m on E, supported in B(0, m + 2) and equal to one on B(0, m + 1).

@[simp]

theorem SchwartzMap.bumpSeq_rIn {E : Type u_1} [NormedAddCommGroup E] (m : ℕ) : (bumpSeq m).rIn = ↑m + 1

The inner radius of bumpSeq m is m + 1.

@[simp]

theorem SchwartzMap.bumpSeq_rOut {E : Type u_1} [NormedAddCommGroup E] (m : ℕ) : (bumpSeq m).rOut = ↑m + 2

The outer radius of bumpSeq m is m + 2.

theorem SchwartzMap.bumpSeq_one_of_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] (m : ℕ) {x : E} (hx : ‖x‖ ≤ ↑m + 1) : ↑(bumpSeq m) x = 1

The bump bumpSeq m is identically 1 on the closed ball of radius m + 1.

theorem SchwartzMap.bumpSeq_hasTemperateGrowth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] (m : ℕ) : Function.HasTemperateGrowth fun (x : E) => ↑(bumpSeq m) x

Each bumpSeq m has temperate growth: it is compactly supported and smooth.

noncomputable def SchwartzMap.bumpCutoffMul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (m : ℕ) (f : SchwartzMap E F) : SchwartzMap E F

Cutoff of a Schwartz function by bumpSeq m: multiplies f pointwise by the bump.

@[simp]

theorem SchwartzMap.bumpCutoffMul_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (m : ℕ) (f : SchwartzMap E F) (x : E) : (bumpCutoffMul m f) x = ↑(bumpSeq m) x • f x

Pointwise formula for the cutoff: bumpCutoffMul m f x = χ_m(x) • f x.

theorem SchwartzMap.bumpCutoffMul_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (m : ℕ) (f : SchwartzMap E F) : HasCompactSupport ⇑(bumpCutoffMul m f)

The cutoff bumpCutoffMul m f has compact support inside B̄(0, m + 2).

theorem SchwartzMap.sub_bumpCutoffMul_eventuallyEq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (m : ℕ) (f : SchwartzMap E F) {x : E} (hx : ‖x‖ < ↑m + 1) : (fun (y : E) => (f - bumpCutoffMul m f) y) =ᶠ[nhds x] fun (x : E) => 0

The difference f - χ_m f vanishes in a neighbourhood of any point inside B(0, m + 1), since χ_m ≡ 1 there.

theorem SchwartzMap.iteratedFDeriv_sub_bumpCutoffMul_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (m : ℕ) (f : SchwartzMap E F) (n : ℕ) {x : E} (hx : ‖x‖ < ↑m + 1) : iteratedFDeriv ℝ n (fun (y : E) => (f - bumpCutoffMul m f) y) x = 0

All iterated Fréchet derivatives of f - χ_m f vanish on B(0, m + 1).

theorem SchwartzMap.seminorm_le_div_of_vanish {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝕜 : Type u_5) [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (g : SchwartzMap E F) (k j : ℕ) (R : ℝ) (hR : 0 < R) (hvanish : ∀ (x : E), ‖x‖ < R → iteratedFDeriv ℝ j (⇑g) x = 0) : (SchwartzMap.seminorm 𝕜 k j) g ≤ (SchwartzMap.seminorm 𝕜 (k + 1) j) g / R

If the j-th iterated derivative of a Schwartz map g vanishes on B(0, R), then the (k, j)-Schwartz seminorm is bounded by the (k + 1, j)-seminorm divided by R.

theorem ContDiffBump.norm_iteratedFDeriv_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] (n : ℕ) (R_bound : ℝ) (hR : 1 < R_bound) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : ContDiffBump 0), f.rOut / f.rIn ≤ R_bound → ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N (↑f) x‖ ≤ C

Iterated Fréchet derivatives of a ContDiffBump on E admit a uniform bound C depending only on the order n and the ratio rOut/rIn.

theorem SchwartzMap.bumpSeq_iteratedFDeriv_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m N : ℕ), N ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ N (fun (y : E) => ↑(bumpSeq m) y) x‖ ≤ C

The iterated Fréchet derivatives of the bumps bumpSeq m are uniformly bounded in both m and the order N ≤ n by a constant C.

theorem SchwartzMap.seminorm_bumpCutoffMul_le_of_seminorm {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝕜 : Type u_5) [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (k j : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m : ℕ), (SchwartzMap.seminorm 𝕜 k j) (bumpCutoffMul m f) ≤ C

The Schwartz seminorm of χ_m f is bounded uniformly in m by a constant depending only on seminorms of f, via the Leibniz rule and the previous bump bound.

theorem SchwartzMap.bumpCutoffMul_seminorm_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝕜 : Type u_5) [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (k j : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m : ℕ), (SchwartzMap.seminorm 𝕜 k j) (f - bumpCutoffMul m f) ≤ C / (↑m + 1)

Quantitative cutoff convergence: there exists a constant C such that ‖f - χ_m f‖_{k,j} ≤ C / (m + 1) for all m, expressing the geometric rate at which χ_m f → f in the Schwartz topology.

theorem SchwartzMap.seminorm_cutoff_sub_tendsto {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝕜 : Type u_3) [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (k j : ℕ) : Filter.Tendsto (fun (m : ℕ) => (SchwartzMap.seminorm 𝕜 k j) (f - bumpCutoffMul m f)) Filter.atTop (nhds 0)

Cutoff convergence (Melrose Lemma 8.8): every Schwartz seminorm of f - χ_m f tends to 0 as m → ∞, hence χ_m f → f in the Schwartz topology.