def ConvolutionDensity.allPdBound {n : ℕ} : ℕ → (EuclideanSpace ℝ (Fin n) → ℂ) → ℝ → Prop

The predicate allPdBound k f δ asserts that all partial derivatives of f of order ≤ k (taken with respect to standard basis directions) are bounded by δ in norm. Defined recursively in k.

theorem ConvolutionDensity.ckNorm_le_of_allPdBound {n : ℕ} (k : ℕ) (f : EuclideanSpace ℝ (Fin n) → ℂ) (δ : ℝ) : 0 ≤ δ → allPdBound k f δ → TestFunctions.ckNorm n k f ≤ (↑n + 1) ^ k * δ

If all partial derivatives of f of order ≤ k are bounded by δ, then the Cᵏ norm is bounded by (n+1)^k · δ.

theorem ConvolutionDensity.allPdBound_of_iteratedFDeriv_le {n : ℕ} (k : ℕ) (f : EuclideanSpace ℝ (Fin n) → ℂ) (δ : ℝ) : ContDiff ℝ (↑k) f → (∀ m ≤ k, ∀ (x : EuclideanSpace ℝ (Fin n)), ‖iteratedFDeriv ℝ m f x‖ ≤ δ) → allPdBound k f δ

Pointwise bounds on the iterated Fréchet derivatives of f up to order k imply the recursive bound allPdBound k f δ on the (axis-aligned) partial derivatives.

theorem ConvolutionDensity.iteratedFDeriv_cutoff_bound {n : ℕ} (k : ℕ) (u : TestFunctions.ContDiffZeroAtInftyN n k) (δ : ℝ) (hδ : 0 < δ) : ∃ (R : ℝ), 0 < R ∧ ∀ (b : ContDiffBump 0), b.rIn = R → b.rOut = R + 1 → ∀ m ≤ k, ∀ (x : EuclideanSpace ℝ (Fin n)), R ≤ ‖x‖ → ‖iteratedFDeriv ℝ m (fun (x : EuclideanSpace ℝ (Fin n)) => u.toZeroAtInftyContinuousMap x - ↑(↑b x) * u.toZeroAtInftyContinuousMap x) x‖ ≤ δ

For every Cᵏ function u that vanishes at infinity and every δ > 0, there exists a radius R so large that for any smooth bump function with inner radius R and outer radius R + 1, all iterated derivatives of u - φ · u are at most δ in norm outside the ball of radius R.

theorem ConvolutionDensity.allPdBound_cutoff_mul {n : ℕ} (k : ℕ) (u : TestFunctions.ContDiffZeroAtInftyN n k) (δ : ℝ) (hδ : 0 < δ) : ∃ (R : ℝ), 0 < R ∧ ∀ (b : ContDiffBump 0), b.rIn = R → b.rOut = R + 1 → allPdBound k (fun (x : EuclideanSpace ℝ (Fin n)) => u.toZeroAtInftyContinuousMap x - ↑(↑b x) * u.toZeroAtInftyContinuousMap x) δ

Combining iteratedFDeriv_cutoff_bound with allPdBound_of_iteratedFDeriv_le: for every δ > 0, multiplying u by a sufficiently far-out cutoff produces an error whose mixed partial derivatives up to order k are bounded by δ.

theorem ConvolutionDensity.approx_by_compactly_supported_Ck {n : ℕ} (k : ℕ) (u : TestFunctions.ContDiffZeroAtInftyN n k) (ε : ℝ) (hε : 0 < ε) : ∃ (v : EuclideanSpace ℝ (Fin n) → ℂ), HasCompactSupport v ∧ ContDiff ℝ (↑k) v ∧ (TestFunctions.ckNorm n k fun (x : EuclideanSpace ℝ (Fin n)) => u.toZeroAtInftyContinuousMap x - v x) < ε

Density: every Cᵏ function vanishing at infinity can be approximated in Cᵏ norm by a smooth compactly supported function, with error less than any prescribed ε > 0. Concretely, multiply u by a sufficiently far-out bump function.