theorem schwartz_seminorm_cauchy_converges_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (u : ℕ → SchwartzMap E F) (hcauchy : ∀ (K : ℕ), ∀ ε > 0, ∃ (N : ℕ), ∀ (n m : ℕ), N ≤ n → N ≤ m → ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm ℝ m.1 m.2) (u n - u m) < ε) : ∃ (v : SchwartzMap E F), ∀ (K : ℕ), Filter.Tendsto (fun (n : ℕ) => ((Finset.Iic (K, K)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm ℝ m.1 m.2) (u n - v)) Filter.atTop (nhds 0)

Auxiliary completeness statement: a Schwartz-seminorm-Cauchy sequence in 𝓢(E, F) converges to some Schwartz function in every seminorm sup_{|α|,|β|≤K}.

theorem instCompleteSpace_axiom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] : CompleteSpace (SchwartzMap E F)

The Schwartz space 𝓢(E, F) is complete (Melrose Prop. 6.7 / 7.4-adjacent statement), stated as a top-level theorem so it can be reused without depending on instance synthesis.

theorem TemperedDistributions.seminorm_cauchy_of_schwartzDist_cauchy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (u : ℕ → SchwartzMap E F) (hcauchy : ∀ ε > 0, ∃ (N : ℕ), ∀ (n m : ℕ), N ≤ n → N ≤ m → schwartzDist (u n) (u m) < ε) (k : ℕ) (ε : ℝ) : ε > 0 → ∃ (N : ℕ), ∀ (n m : ℕ), N ≤ n → N ≤ m → (supSeminorm k) (u n - u m) < ε

If a sequence in 𝓢(E, F) is Cauchy for the canonical Schwartz metric, then it is Cauchy for every truncated supremum-seminorm supSeminorm k.

instance TemperedDistributions.instCompleteSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] : CompleteSpace (SchwartzMap E F)

Completeness of the Schwartz space 𝓢(E, F) as a Mathlib CompleteSpace instance (Melrose Prop. 6.7).