The cocompact filter on Euclidean space is countably generated: it has a countable basis given by complements of closed balls of integer radius.
Approximate-identity convergence for C₀ functions: if φ i is a family
of nonnegative, integral-one functions whose supports shrink to {0}, then
the convolutions φ i ⋆ f converge uniformly to f for any f ∈ C₀(G, ℝ).
This is a key ingredient for proving density results via mollification.
Density between smoothness classes of C₀ functions: any C^p
zero-at-infinity function can be approximated in the C^p norm by
C^k zero-at-infinity functions whenever p ≤ k.
Mollification threshold in the C^k norm: for any compactly-supported
C^k function v and any ε > 0, there exists a radius r > 0 such that
convolution with any normalised bump of outer radius at most r approximates
v within ε in the C^k norm. The proof proceeds by induction on k,
using uniform continuity of derivatives at the base step and commuting
convolution with fderiv at the inductive step.
Any compactly-supported C^k function on Euclidean space can be
approximated in the C^k norm by a Schwartz function. The approximant is
constructed by convolving v with a sufficiently narrow normalised bump,
which produces a compactly-supported smooth function — and hence a Schwartz
function — within ε of v in the C^k norm.
CkNormBdd n k f is the recursive predicate stating that all derivatives
of f : EuclideanSpace ℝ (Fin n) → ℂ up to order k are bounded; that is,
f is k times differentiable and f together with all its partial
derivatives up to order k have bounded norm ranges.
Instances For
The difference of a C^k zero-at-infinity function and a compactly
supported C^k function has all derivatives up to order k bounded.
The difference of a compactly supported C^k function and a Schwartz
function has all derivatives up to order k bounded.
Base case of the triangle inequality for the C^k norm: at order zero,
the supremum norm satisfies ‖f + g‖_∞ ≤ ‖f‖_∞ + ‖g‖_∞ whenever each is
bounded above.
Triangle inequality for the C^k norm: for functions with bounded
derivatives up to order k, the C^k norm of a sum is at most the sum of
the C^k norms. Proved by induction on k using linearity of fderiv on
sums of differentiable functions.
Schwartz functions are dense in the space of C^k zero-at-infinity
functions: any such u can be approximated in the C^k norm to within ε
by a Schwartz function. The proof first approximates u by a compactly
supported C^k function, then approximates that by a Schwartz function via
mollification.
Continuity of translation in L²: for u ∈ L²(ℝⁿ), the L² norm of
u(· + t) - u(·) tends to 0 as t → 0. This is the standard "continuity
in mean" property of L^p spaces.
Two finite measures on Euclidean space are equal if they integrate every Schwartz function to the same value: Schwartz functions form a separating family for finite measures.
Multiplication by a compactly-supported function on the left preserves compact support.
General-target form: the compactly-supported Schwartz functions
𝓢(E, F) are dense in 𝓢(E, F). The proof uses bump-cutoff multiplication
and the convergence of the corresponding Schwartz seminorms.
Multiplication of a Schwartz function f by a compactly-supported smooth
real-valued function φ. The result is again Schwartz with compact support
contained in the support of φ.
Instances For
Pointwise evaluation of SchwartzMap.cutoffMul: at each x, the cut-off
product equals φ x • f x.
The Plancherel isometry: the L² Fourier transform on a real
finite-dimensional inner product space V is a ℂ-linear isometric
equivalence of L²(V; ℂ) with itself. This is the operator-theoretic
incarnation of the Plancherel theorem.