def ConvergesPointwise (f : ℕ → ℝ → ℝ) (g : ℝ → ℝ) (S : Set ℝ) : Prop

ConvergesPointwise f g S states that the sequence of functions f n converges pointwise to g on S: for every x ∈ S, the sequence f n x tends to g x as n → ∞.

theorem uniform_convergence_iff (f : ℕ → ℝ → ℝ) (g : ℝ → ℝ) (S : Set ℝ) : TendstoUniformlyOn f g Filter.atTop S ↔ ∀ ε > 0, ∃ (M : ℕ), ∀ n ≥ M, ∀ x ∈ S, |f n x - g x| < ε

Uniform convergence of f n to g on S is equivalent to the classical ε-M formulation: for every ε > 0, there exists M ∈ ℕ such that for all n ≥ M and all x ∈ S, |f n x - g x| < ε.

theorem weierstrass_m_test (f : ℕ → ℝ → ℝ) (M : ℕ → ℝ) (S : Set ℝ) (hM : ∀ (j : ℕ), ∀ x ∈ S, |f j x| ≤ M j) (hMsum : Summable M) : (∀ x ∈ S, Summable fun (j : ℕ) => f j x) ∧ TendstoUniformlyOn (fun (n : ℕ) (x : ℝ) => ∑ j ∈ Finset.range n, f j x) (fun (x : ℝ) => ∑' (j : ℕ), f j x) Filter.atTop S

Weierstrass M-test: if |f j x| ≤ M j for all j and all x ∈ S, and ∑ M j converges, then for every x ∈ S the series ∑ f j x converges (absolutely), and the partial sums ∑_{j < n} f j x converge uniformly on S to ∑' j, f j x.