theorem all_cauchy_implies_cauchySeq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (u : ℕ → SchwartzMap E F) (hcauchy : ∀ (k n : ℕ), ∀ ε > 0, ∃ (N : ℕ), ∀ (a b : ℕ), N ≤ a → N ≤ b → (SchwartzMap.seminorm ℝ k n) (u a - u b) < ε) : CauchySeq u

A sequence of Schwartz functions is Cauchy in the Schwartz topology whenever it is Cauchy with respect to every individual seminorm ‖·‖_{k,n}.

theorem diag_cauchy_implies_cauchySeq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ 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) < ε) : CauchySeq u

"Diagonal" version of all_cauchy_implies_cauchySeq: testing Cauchyness against the finite-supremum seminorm sup_{(p, q) ≤ (K, K)} ‖·‖_{p,q} for every K is enough.

theorem SchwartzMap.cauchySeq_seminorm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (u : ℕ → SchwartzMap E F) (hu : CauchySeq u) (k n : ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m l : ℕ), N ≤ m → N ≤ l → (SchwartzMap.seminorm ℝ k n) (u m - u l) < ε

A Cauchy sequence in the Schwartz space is Cauchy with respect to every individual seminorm ‖·‖_{k,n}.

theorem iterFDeriv_sub_le_seminorm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (u : ℕ → SchwartzMap E F) (n m l : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (⇑(u m)) x - iteratedFDeriv ℝ n (⇑(u l)) x‖ ≤ (SchwartzMap.seminorm ℝ 0 n) (u m - u l)

The pointwise difference between the n-th iterated derivatives of two Schwartz functions is dominated by the Schwartz seminorm ‖u m - u l‖_{0, n}.

theorem schwartz_cauchySeq_limit_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (u : ℕ → SchwartzMap E F) (hu : CauchySeq u) : ∃ (g : E → F), ContDiff ℝ (↑⊤) g ∧ ∀ (n : ℕ) (x : E), Filter.Tendsto (fun (m : ℕ) => iteratedFDeriv ℝ n (⇑(u m)) x) Filter.atTop (nhds (iteratedFDeriv ℝ n g x))

The pointwise limit g of a Cauchy sequence of Schwartz functions is smooth, and its iterated derivatives are the pointwise limits of the iterated derivatives of the sequence.

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

Melrose Proposition 6.7 (Schwartz completeness): the Schwartz space 𝓢(E, F) is complete whenever the target F is complete.