def finiteSumRealFunctions {X : Type u_1} {N : ℕ} (f : Fin N → X → ℝ) : X → ℝ

Definition 3.8: (Finite sum of real-valued functions) Let (X,d_X) be a metric space and let f^{(1)},...,f^{(N)} : X -> Real. The finite sum sum_{i=1}^N f^{(i)} : X -> Real is defined by (sum_{i=1}^N f^{(i)})(x) = sum_{i=1}^N f^{(i)}(x).

Equations

• finiteSumRealFunctions f x = ∑ i : Fin N, f i x

def example351_fi : Fin 3 → ℝ → ℝ

The family of three functions x, x^2, and x^3 indexed by Fin 3.

Equations

• example351_fi = ![fun (x : ℝ) => x, fun (x : ℝ) => x ^ 2, fun (x : ℝ) => x ^ 3]

def example351_f : ℝ → ℝ

Example 3.5.1: Let f^{(1)}(x) = x, f^{(2)}(x) = x^2, and f^{(3)}(x) = x^3. Define f := ∑_{i=1}^3 f^{(i)}, so that f(x) = x + x^2 + x^3.

Equations

• example351_f = finiteSumRealFunctions example351_fi

theorem example351_f_apply (x : ℝ) : example351_f x = x + x ^ 2 + x ^ 3

The finite sum of example351_fi evaluates to x + x^2 + x^3.

theorem helperForText_3_5_2_chooseData {X : Type u_1} {Y : Type u_2} [Nonempty X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {n : ℕ} (f : Fin n → X → Y) (hfb : ∀ (i : Fin n), ∃ (y0 : Y) (M : ℝ), ∀ (x : X), dist (f i x) y0 ≤ M) : ∃ (c : Fin n → Y) (B : Fin n → ℝ), ∀ (i : Fin n) (x : X), dist (f i x) (c i) ≤ B i

Helper for Text 3.5.2: choose centers and bounds for a bounded family.

theorem helperForText_3_5_2_dist_le_maxBound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {n : ℕ} {f : Fin n → X → Y} {c : Fin n → Y} {B : Fin n → ℝ} {i : Fin n} {x : X} (h : dist (f i x) (c i) ≤ B i) : dist (f i x) (c i) ≤ max (B i) 0

Helper for Text 3.5.2: extend a pointwise bound to max (B i) 0.

theorem helperForText_3_5_2_dist_sum_sum_le {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {n : ℕ} (f : Fin n → X → Y) (c : Fin n → Y) (x : X) : dist (∑ i : Fin n, f i x) (∑ i : Fin n, c i) ≤ ∑ i : Fin n, dist (f i x) (c i)

Helper for Text 3.5.2: dist between sums is bounded by sum of pointwise dists.

theorem helperForText_3_5_2_sum_dist_le_sum_max {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {n : ℕ} (f : Fin n → X → Y) (c : Fin n → Y) (B : Fin n → ℝ) (hcB : ∀ (i : Fin n) (x : X), dist (f i x) (c i) ≤ B i) (x : X) : ∑ i : Fin n, dist (f i x) (c i) ≤ ∑ i : Fin n, max (B i) 0

Helper for Text 3.5.2: sum of pointwise dists is bounded by sum of max bounds.

theorem finiteSum_boundedFunctions {X : Type u_1} {Y : Type u_2} [Nonempty X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {n : ℕ} (f : Fin n → X → Y) (hfb : ∀ (i : Fin n), ∃ (y0 : Y) (M : ℝ), ∀ (x : X), dist (f i x) y0 ≤ M) : ∃ (y0 : Y) (M : ℝ), ∀ (x : X), dist (∑ i : Fin n, f i x) y0 ≤ M

Text 3.5.2: [Finite sums of bounded functions are bounded] Let X be a nonempty set and let (Y, d_Y) be a metric space, with Y a normed vector space and d_Y(u,v)=‖u-v‖. If f^{(1)}, …, f^{(n)} ∈ B(X → Y), then the pointwise sum f(x)=∑_{i=1}^n f^{(i)}(x) is bounded, hence f ∈ B(X → Y).

theorem finiteSum_continuousFunctions {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {n : ℕ} (f : Fin n → X → Y) (hfc : ∀ (i : Fin n), Continuous (f i)) : Continuous fun (x : X) => ∑ i : Fin n, f i x

Text 3.5.3: [Finite sums of continuous functions are continuous] Let (X, d_X) be a metric space and let Y be a normed vector space (with its metric). If f^{(1)}, …, f^{(n)} : X → Y are continuous, then f := ∑_{i=1}^n f^{(i)} is continuous.

inductive SeriesConvergenceMode : Type

Convergence mode for a series of functions: pointwise or uniform.

• pointwise : SeriesConvergenceMode
• uniform : SeriesConvergenceMode

def seriesPartialSum {X : Type u_1} (f : ℕ → X → ℝ) (N : ℕ) : X → ℝ

Partial sum function S_N(x) = ∑_{n=1}^N f^{(n)}(x).

Equations

• seriesPartialSum f N x = ∑ n ∈ Finset.Icc 1 N, f n x

def seriesConverges {X : Type u_1} [MetricSpace X] (f : ℕ → X → ℝ) (g : X → ℝ) (mode : SeriesConvergenceMode) : Prop

Definition 3.9: [Infinite series of functions] Let (X,d_X) be a metric space and let (f^{(n)})_{n≥1} be functions f^{(n)} : X → ℝ, with partial sums S_N(x) = ∑_{n=1}^N f^{(n)}(x). Let f : X → ℝ. (i) The series ∑_{n=1}^∞ f^{(n)} converges pointwise to f on X if for every x ∈ X, lim_{N→∞} S_N(x) = f(x). (ii) The series converges uniformly to f on X if S_N → f uniformly on X, i.e. lim_{N→∞} sup_{x∈X} |S_N(x) - f(x)| = 0.

Equations

• seriesConverges f g SeriesConvergenceMode.pointwise = ∀ (x : X), Filter.Tendsto (fun (N : ℕ) => seriesPartialSum f N x) Filter.atTop (nhds (g x))
• seriesConverges f g SeriesConvergenceMode.uniform = TendstoUniformly (fun (N : ℕ) => seriesPartialSum f N) g Filter.atTop

def IsBoundedRealFunction {X : Type u_1} (f : X → ℝ) : Prop

A real-valued function on X is bounded if there exists M ≥ 0 with |f x| ≤ M for all x.

Equations

• IsBoundedRealFunction f = ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : X), |f x| ≤ M

noncomputable def supNorm {X : Type u_1} (f : { f : X → ℝ // IsBoundedRealFunction f }) : ℝ

Definition 3.10: [Sup norm] Let X be a set and let f : X → ℝ be bounded. The sup norm (uniform norm) is ‖f‖∞ = sup { |f(x)| : x ∈ X }, and if X = ∅ then ‖f‖∞ = 0.

Equations

• supNorm f = sSup (Set.range fun (x : X) => |↑f x|)

theorem helperForText_3_5_4_bddAbove_range_abs {X : Type u_1} (f : { f : X → ℝ // IsBoundedRealFunction f }) : BddAbove (Set.range fun (x : X) => |↑f x|)

Helper for Text 3.5.4: bounded above range of absolute values.

theorem helperForText_3_5_4_abs_le_supNorm {X : Type u_1} (f : { f : X → ℝ // IsBoundedRealFunction f }) (x : X) : |↑f x| ≤ supNorm f

Helper for Text 3.5.4: pointwise bound by the sup norm.

theorem supNorm_nonneg {X : Type u_1} [Nonempty X] (f : { f : X → ℝ // IsBoundedRealFunction f }) : 0 ≤ supNorm f

Text 3.5.4: [Finiteness and nonnegativity of the sup norm] Let X be a nonempty set and let f : X → ℝ be bounded. Define ‖f‖∞ := sup_{x∈X} |f(x)|. Then ‖f‖∞ ∈ [0,∞), in particular it is finite and nonnegative.

theorem helperForTheorem_3_5_seriesPartialSum_eq_sum_range_succ {X : Type u_1} (f : ℕ → X → ℝ) (N : ℕ) (x : X) : seriesPartialSum f N x = ∑ n ∈ Finset.range N, f (n + 1) x

Helper for Theorem 3.5: rewrite seriesPartialSum as a Finset.range sum.

theorem helperForTheorem_3_5_norm_le_supNorm {X : Type u_1} {f0 : X → ℝ} (hbf : IsBoundedRealFunction f0) (x : X) : ‖f0 x‖ ≤ supNorm ⟨f0, hbf⟩

Helper for Theorem 3.5: pointwise norm bound by the sup norm.

theorem helperForTheorem_3_5_tendstoUniformly_seriesPartialSum_tsum {X : Type u_1} [MetricSpace X] (f : ℕ → X → ℝ) (hbounded : ∀ (n : ℕ), IsBoundedRealFunction (f n)) (hsum : Summable fun (n : ℕ) => supNorm ⟨f n, ⋯⟩) : TendstoUniformly (fun (N : ℕ) => seriesPartialSum f N) (fun (x : X) => ∑' (n : ℕ), f (n + 1) x) Filter.atTop

Helper for Theorem 3.5: uniform convergence of partial sums to the tsum.

theorem helperForTheorem_3_5_seriesPartialSum_continuous {X : Type u_1} [MetricSpace X] (f : ℕ → X → ℝ) (hcont : ∀ (n : ℕ), Continuous (f n)) (N : ℕ) : Continuous (seriesPartialSum f N)

Helper for Theorem 3.5: continuity of each partial sum.

theorem weierstrass_M_test {X : Type u_1} [MetricSpace X] (f : ℕ → X → ℝ) (hcont : ∀ (n : ℕ), Continuous (f n)) (hbounded : ∀ (n : ℕ), IsBoundedRealFunction (f n)) (hsum : Summable fun (n : ℕ) => supNorm ⟨f n, ⋯⟩) : ∃ (g : X → ℝ), seriesConverges f g SeriesConvergenceMode.uniform ∧ Continuous g

Theorem 3.5: [Weierstrass M-test] Let (X,d) be a metric space and let (f^{(n)}) be a sequence of bounded real-valued continuous functions on X. Assume the series ∑ ‖f^{(n)}‖∞ converges. Then the series of functions ∑ f^{(n)} converges uniformly on X to a function f : X → ℝ, and f is continuous on X.

def geometricSeriesTermOnIoo (n : ℕ) (x : { x : ℝ // x ∈ Set.Ioo (-1) 1 }) : ℝ

The geometric series term function on (-1,1) given by x ↦ x^n.

Equations

• geometricSeriesTermOnIoo n x = ↑x ^ n

noncomputable def geometricSeriesSumOnIoo (x : { x : ℝ // x ∈ Set.Ioo (-1) 1 }) : ℝ

The geometric series sum function on (-1,1) given by x ↦ x/(1-x).

Equations

• geometricSeriesSumOnIoo x = ↑x / (1 - ↑x)

theorem helperForExample_3_5_2_seriesPartialSum_closedForm (x : { x : ℝ // x ∈ Set.Ioo (-1) 1 }) (N : ℕ) : seriesPartialSum geometricSeriesTermOnIoo N x = (↑x - ↑x ^ (N + 1)) / (1 - ↑x)

Helper for Example 3.5.2: closed form for the geometric series partial sum on (-1,1).

theorem helperForExample_3_5_2_dist_to_limit_closedForm (x : { x : ℝ // x ∈ Set.Ioo (-1) 1 }) (N : ℕ) : dist (seriesPartialSum geometricSeriesTermOnIoo N x) (geometricSeriesSumOnIoo x) = |↑x ^ (N + 1) / (1 - ↑x)|

Helper for Example 3.5.2: distance from partial sum to limit in closed form.

theorem helperForExample_3_5_2_pointwiseConvergence : seriesConverges geometricSeriesTermOnIoo geometricSeriesSumOnIoo SeriesConvergenceMode.pointwise

Helper for Example 3.5.2: pointwise convergence of the geometric series on (-1,1).

noncomputable def helperForExample_3_5_2_xNValue (N : ℕ) : ℝ

Helper for Example 3.5.2: explicit real value x_N = 1 - 1/2^(N+1).

Equations

• helperForExample_3_5_2_xNValue N = 1 - 1 / 2 ^ (N + 1)

theorem helperForExample_3_5_2_xN_ge_half (N : ℕ) : 1 / 2 ≤ helperForExample_3_5_2_xNValue N

Helper for Example 3.5.2: the point x_N is at least 1/2.

theorem helperForExample_3_5_2_xN_mem (N : ℕ) : helperForExample_3_5_2_xNValue N ∈ Set.Ioo (-1) 1

Helper for Example 3.5.2: the point x_N lies in (-1,1).

theorem helperForExample_3_5_2_counterexample_large_error (N : ℕ) : ∃ (x : { x : ℝ // x ∈ Set.Ioo (-1) 1 }), 1 / 2 ≤ dist (seriesPartialSum geometricSeriesTermOnIoo N x) (geometricSeriesSumOnIoo x)

Helper for Example 3.5.2: for each N, some point has error at least 1/2.

theorem example352_pointwise_not_uniform : seriesConverges geometricSeriesTermOnIoo geometricSeriesSumOnIoo SeriesConvergenceMode.pointwise ∧ ¬seriesConverges geometricSeriesTermOnIoo geometricSeriesSumOnIoo SeriesConvergenceMode.uniform

Example 3.5.2: Pointwise but not uniform convergence of a geometric series. For f^{(n)}(x) = x^n on (-1,1), the series converges pointwise to x/(1-x), but the convergence is not uniform on (-1,1).

theorem seriesConverges_pointwise_of_uniform {X : Type u_1} [MetricSpace X] (f : ℕ → X → ℝ) (g : X → ℝ) : seriesConverges f g SeriesConvergenceMode.uniform → seriesConverges f g SeriesConvergenceMode.pointwise

Proposition 3.17: If a series of functions converges uniformly to f on X, then it converges pointwise to f on X.

def example356_X : Type

The interval (-2,1) as a subtype of ℝ.

Equations

• example356_X = { x : ℝ // x ∈ Set.Ioo (-2) 1 }

def example356_f : example356_X → ℝ

The function x ↦ 2x on (-2,1).

Equations

• example356_f x = 2 * ↑x

theorem example356_f_bounded : IsBoundedRealFunction example356_f

The function x ↦ 2x on (-2,1) is bounded.

def example356_f_boundedSubtype : { f : example356_X → ℝ // IsBoundedRealFunction f }

The bounded function x ↦ 2x on (-2,1) packaged for supNorm.

Equations

• example356_f_boundedSubtype = ⟨example356_f, example356_f_bounded⟩

theorem example356_abs_value_le_four (x : example356_X) : |example356_f x| ≤ 4

Pointwise bound for |2x| on (-2,1).

theorem example356_delta_point_mem_Ioo (a : ℝ) (ha : a < 4) : have δ := min ((4 - a) / 4) 1; -2 + δ ∈ Set.Ioo (-2) 1

A canonical point near -2 that still lies in (-2,1).

theorem example356_exists_abs_gt_of_lt_four (a : ℝ) (ha : a < 4) : ∃ (x : example356_X), a < |example356_f x|

Any level strictly below 4 is exceeded by |2x| at some point of (-2,1).

theorem example356_supNorm_le_four : supNorm example356_f_boundedSubtype ≤ 4

Upper bound ‖x ↦ 2x‖∞ ≤ 4 on (-2,1).

theorem example356_supNorm_eq : supNorm example356_f_boundedSubtype = 4

Example 3.5.6: (Computing the sup norm) For X = (-2,1) and f(x) = 2x, the sup norm ‖f‖∞ = sup_{x∈X} |f(x)| equals 4.

def geometricSeriesTermOnIcc (r : ℝ) (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc (-r) r }) : ℝ

The geometric series term function on [-r,r] given by x ↦ x^n.

Equations

• geometricSeriesTermOnIcc r n x = ↑x ^ n

noncomputable def geometricSeriesSumOnIcc (r : ℝ) (x : { x : ℝ // x ∈ Set.Icc (-r) r }) : ℝ

The geometric series sum function on [-r,r] given by x ↦ x/(1-x).

Equations

• geometricSeriesSumOnIcc r x = ↑x / (1 - ↑x)

theorem helperForExample_3_5_8_abs_coe_le_r {r : ℝ} (x : { x : ℝ // x ∈ Set.Icc (-r) r }) : |↑x| ≤ r

Helper for Example 3.5.8: bound |x| by r on [-r,r].

theorem helperForExample_3_5_8_abs_pow_le_r_pow {r : ℝ} (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc (-r) r }) : |↑x ^ n| ≤ r ^ n

Helper for Example 3.5.8: bound |x^n| by r^n on [-r,r].

theorem helperForExample_3_5_8_supNorm_term_eq_r_pow {r : ℝ} (hr0 : 0 < r) (n : ℕ) (h : IsBoundedRealFunction (geometricSeriesTermOnIcc r n)) : supNorm ⟨geometricSeriesTermOnIcc r n, h⟩ = r ^ n

Helper for Example 3.5.8: compute ‖x ↦ x^n‖∞ on [-r,r].

theorem helperForExample_3_5_8_tsum_pow_succ_eq_div {x : ℝ} (hx : |x| < 1) : ∑' (n : ℕ), x ^ (n + 1) = x / (1 - x)

Helper for Example 3.5.8: shifted geometric series on |x| < 1.

theorem example358_uniform_convergence_geometric_on_Icc {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) : (∀ (n : ℕ), Continuous (geometricSeriesTermOnIcc r n)) ∧ (∀ (n : ℕ), IsBoundedRealFunction (geometricSeriesTermOnIcc r n)) ∧ (∀ (n : ℕ), ∃ (h : IsBoundedRealFunction (geometricSeriesTermOnIcc r n)), supNorm ⟨geometricSeriesTermOnIcc r n, h⟩ = r ^ n) ∧ seriesConverges (geometricSeriesTermOnIcc r) (geometricSeriesSumOnIcc r) SeriesConvergenceMode.uniform ∧ Continuous (geometricSeriesSumOnIcc r) ∧ seriesConverges geometricSeriesTermOnIoo geometricSeriesSumOnIoo SeriesConvergenceMode.pointwise ∧ ¬seriesConverges geometricSeriesTermOnIoo geometricSeriesSumOnIoo SeriesConvergenceMode.uniform

Example 3.5.8: [Uniform convergence on [-r,r] for a geometric series] Let 0 < r < 1 and define f^{(n)}(x) = x^n on [-r,r]. Each f^{(n)} is continuous and bounded, with sup norm ‖f^{(n)}‖∞ = r^n. The series ∑ f^{(n)} converges uniformly on [-r,r] to x/(1-x), and ∑ x^n is pointwise but not uniformly convergent on (-1,1).