The supremum of all Schwartz seminorms ‖·‖_{m₁, m₂} for m₁, m₂ ≤ k.
Instances For
The supSeminorm is nonnegative.
Each individual Schwartz seminorm ‖·‖_{k, n} with k, n ≤ K is bounded by supSeminorm K.
The k-th term in the metric series: 2⁻ᵏ · s/(1+s) where s is the k-th supremum
seminorm of u - v.
Instances For
Each boundedSeminormTerm is nonnegative.
Each boundedSeminormTerm is bounded above by (1/2)^k.
The series of boundedSeminormTerm values is summable, since it is dominated by the geometric
series ∑ (1/2)^k.
Triangle inequality for each metric term: boundedSeminormTerm k u w ≤ boundedSeminormTerm k u v + boundedSeminormTerm k v w.
The Schwartz metric: schwartzDist u v = ∑ₖ 2⁻ᵏ · sₖ(u - v) / (1 + sₖ(u - v)) where sₖ
is the k-th sup seminorm.
Instances For
Each individual term of the metric series is bounded by the full Schwartz distance.
The Schwartz distance is nonnegative.
Self-distance is zero: schwartzDist u u = 0.
Symmetry of the Schwartz metric: schwartzDist u v = schwartzDist v u.
Triangle inequality for the Schwartz metric:
schwartzDist u w ≤ schwartzDist u v + schwartzDist v w.
Identity of indiscernibles: schwartzDist u v = 0 ↔ u = v.
The norm of boundedSeminormTerm k u v is bounded by (1/2)^k.
If a nonnegative sequence tends to zero, then so does the bounded transform s / (1 + s).
If supSeminorm k (uₙ - v) → 0, then boundedSeminormTerm k (uₙ) v → 0.
A schwartzDist-Cauchy sequence is Cauchy with respect to each supSeminorm k.
A sequence Cauchy in every Finset.Iic (K, K) sup-seminorm converges to some Schwartz
function v in each of those seminorms.
If supSeminorm k (uₙ - v) → 0 for every k, then schwartzDist (uₙ) v → 0, by dominated
convergence applied to the geometric majorant.
Completeness of the Schwartz metric: every schwartzDist-Cauchy sequence converges to some
Schwartz function.
Bundled metric axioms for the Schwartz distance (Proposition 6.7 of Melrose): identity, symmetry, triangle inequality, separation, and completeness.