def PointwiseConvergent {X : Type u_1} {Y : Type u_2} [MetricSpace Y] (f : ℕ → X → Y) (g : X → Y) : Prop

Definition 3.2: Pointwise convergence. A sequence of functions f converges pointwise to g on X if for every x, the sequence n ↦ f n x tends to g x (equivalently: for every x and ε > 0 there exists N such that for all n ≥ N, dist (f n x) (g x) < ε).

Equations

• PointwiseConvergent f g = ∀ (x : X), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))

theorem tendsto_const_div_nat_atTop (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => x / ↑n) Filter.atTop (nhds 0)

Example 3.2.3: for any fixed x ∈ ℝ, the sequence n ↦ x / n converges to 0 as n → ∞.

theorem helperForExample_3_2_4_abs_lt_one_of_nonneg_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h : r < 1) : |r| < 1

Helper for Example 3.2.4: if 0 ≤ r < 1 then |r| < 1.

theorem helperForExample_3_2_4_eq_one_of_le_one_of_not_lt_one {r : ℝ} (hr : r ≤ 1) (h : ¬r < 1) : r = 1

Helper for Example 3.2.4: if r ≤ 1 and ¬ r < 1, then r = 1.

theorem pointwiseConvergent_pow_on_unitInterval : PointwiseConvergent (fun (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => ↑x ^ n) fun (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => if ↑x < 1 then 0 else 1

Example 3.2.4: for f^{(n)}(x) := x^n on [0,1], the pointwise limit f is given by f(x) = 0 for 0 ≤ x < 1 and f(1) = 1.

theorem helperForExample_3_2_5_nhdsWithin_Ico_neBot : (nhdsWithin 1 (Set.Ico 0 1)).NeBot

Helper for Example 3.2.5: the within-neighborhood filter on Ico 0 1 at 1 is nontrivial.

theorem pointwiseConvergence_not_preserve_limit_on_Ico : (∀ (n : ℕ), Filter.Tendsto (fun (x : ℝ) => x ^ n) (nhdsWithin 1 (Set.Ico 0 1)) (nhds 1)) ∧ (∀ x ∈ Set.Ico 0 1, Filter.Tendsto (fun (n : ℕ) => x ^ n) Filter.atTop (nhds 0)) ∧ Filter.Tendsto (fun (x : ℝ) => 0) (nhdsWithin 1 (Set.Ico 0 1)) (nhds 0) ∧ ¬Filter.Tendsto (fun (x : ℝ) => 0) (nhdsWithin 1 (Set.Ico 0 1)) (nhds 1)

Example 3.2.5: for f^{(n)}(x) = x^n on [0,1), each f^{(n)} has limit 1 as x → 1 within [0,1), while the pointwise limit on [0,1) is 0, so iterated limits need not agree and pointwise convergence does not preserve limits.

noncomputable def spikeFunction (n : ℕ) (x : ℝ) : ℝ

A spike function on [0,1] used in a pointwise-convergence counterexample.

Equations

• spikeFunction n x = if x ∈ Set.Icc (1 / (2 * (↑n + 1))) (1 / (↑n + 1)) then 2 * (↑n + 1) else 0

theorem helperForExample_3_2_6_spikeFunction_as_indicator (n : ℕ) : spikeFunction n = (Set.Icc (1 / (2 * (↑n + 1))) (1 / (↑n + 1))).indicator fun (x : ℝ) => 2 * (↑n + 1)

Helper for Example 3.2.6: rewrite spikeFunction as an indicator of an interval.

theorem helperForExample_3_2_6_endpoints_properties (n : ℕ) : 0 < 1 / (2 * (↑n + 1)) ∧ 1 / (2 * (↑n + 1)) ≤ 1 / (↑n + 1) ∧ 1 / (↑n + 1) ≤ 1

Helper for Example 3.2.6: basic inequalities for the spike interval endpoints.

theorem helperForExample_3_2_6_eventually_spikeFunction_eq_zero (x : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, spikeFunction n x = 0

Helper for Example 3.2.6: the spike functions are eventually zero at each point.

theorem helperForExample_3_2_6_intervalIntegrable_spikeFunction (n : ℕ) : IntervalIntegrable (spikeFunction n) MeasureTheory.volume 0 1

Helper for Example 3.2.6: the spike functions are interval integrable on [0,1].

theorem helperForExample_3_2_6_intervalIntegral_spikeFunction (n : ℕ) : ∫ (x : ℝ) in 0..1, spikeFunction n x = 1

Helper for Example 3.2.6: the spike interval integral equals 1.

theorem counterexample_pointwiseIntegral_limit : (PointwiseConvergent spikeFunction fun (x : ℝ) => 0) ∧ (∀ (n : ℕ), IntervalIntegrable (spikeFunction n) MeasureTheory.volume 0 1) ∧ (∀ (n : ℕ), ∫ (x : ℝ) in 0..1, spikeFunction n x = 1) ∧ ∫ (x : ℝ) in 0..1, 0 = 0 ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in 0..1, spikeFunction n x) Filter.atTop (nhds 1) ∧ 1 ≠ 0

Example 3.2.6: the spike functions on [0,1] converge pointwise to 0, each has integral 1, and hence the limit of the integrals is not the integral of the pointwise limit.

noncomputable def movingBump (n : ℕ) (x : ℝ) : ℝ

A moving bump function on ℝ given by the indicator of [n, n+1].

Equations

• movingBump n x = if x ∈ Set.Icc (↑n) (↑n + 1) then 1 else 0

theorem helperForExample_3_2_7_movingBump_eq_indicator (n : ℕ) : movingBump n = (Set.Icc (↑n) (↑n + 1)).indicator 1

Helper for Example 3.2.7: movingBump is the indicator of [n, n+1].

theorem helperForExample_3_2_7_eventually_movingBump_eq_zero (x : ℝ) : (fun (n : ℕ) => movingBump n x) =ᶠ[Filter.atTop] fun (x : ℕ) => 0

Helper for Example 3.2.7: for fixed x, the moving bump is eventually zero.

theorem helperForExample_3_2_7_volume_real_Icc_nat (n : ℕ) : MeasureTheory.volume.real (Set.Icc (↑n) (↑n + 1)) = 1

Helper for Example 3.2.7: the Lebesgue measure of [n, n+1] is 1.

theorem helperForExample_3_2_7_integral_movingBump (n : ℕ) : ∫ (x : ℝ), movingBump n x = 1

Helper for Example 3.2.7: the integral of movingBump n is 1.

theorem movingBump_pointwiseIntegral_counterexample : (PointwiseConvergent movingBump fun (x : ℝ) => 0) ∧ (∀ (n : ℕ), ∫ (x : ℝ), movingBump n x = 1) ∧ ∫ (x : ℝ), 0 = 0 ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), movingBump n x) Filter.atTop (nhds 1) ∧ 1 ≠ 0

Example 3.2.7: [Moving bump: pointwise convergence does not commute with integration] for f_n the indicator of [n, n+1], (1) f_n(x) → 0 pointwise on ℝ, (2) ∫ f_n = 1 for all n, and (3) ∫ (lim_n f_n) = 0, hence lim_n ∫ f_n ≠ ∫ lim_n f_n.

theorem pointwiseConvergent_pow_on_Icc_zero_one : PointwiseConvergent (fun (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => ↑x ^ n) fun (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => if ↑x < 1 then 0 else 1

Example 3.2.8: [Pointwise limit of x^n on [0,1]]. For f_n(x) = x^n on [0,1], the pointwise limit is f(x) = 0 for 0 ≤ x < 1 and f(1) = 1.

theorem helperForExample_3_2_9_limitValue_at_two : (if 2 < 1 then 0 else 1) = 1

Helper for Example 3.2.9: the pointwise limit evaluates to 1 at x = 2.

theorem helperForExample_3_2_9_not_tendsto_pow_two_nhds_one : ¬Filter.Tendsto (fun (n : ℕ) => 2 ^ n) Filter.atTop (nhds 1)

Helper for Example 3.2.9: the sequence 2^n does not converge to 1.

theorem not_tendstoUniformly_pow_on_Icc_zero_one : ¬TendstoUniformly (fun (n : ℕ) (x : ℝ) => x ^ n) (fun (x : ℝ) => if x < 1 then 0 else 1) Filter.atTop

Example 3.2.9: [x^n does not converge uniformly on [0,1]]. Let f_n(x) = x^n on [0,1], and let f be the pointwise limit above. Then f_n does not converge uniformly to f on [0,1].

def UniformlyConvergent {X : Type u_1} {Y : Type u_2} [MetricSpace Y] (f : ℕ → X → Y) (g : X → Y) : Prop

Definition 3.3: Uniform convergence. A sequence f converges uniformly to g on X if for every ε > 0 there exists N such that for all n ≥ N and all x, dist (f n x) (g x) < ε. In this case, g is the uniform limit of the sequence.

Equations

• UniformlyConvergent f g = TendstoUniformly f g Filter.atTop

theorem uniformlyConvergent_implies_pointwiseConvergent {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : ℕ → X → Y) (g : X → Y) : UniformlyConvergent f g → PointwiseConvergent f g

Example 3.2.10: if a sequence of functions converges uniformly to f on X, then it converges pointwise to f on X.

theorem helperForExample_3_2_11_abs_val_le_one (x : { x : ℝ // x ∈ Set.Icc 0 1 }) : |↑x| ≤ 1

Helper for Example 3.2.11: points in [0,1] have absolute value at most 1.

theorem helperForExample_3_2_11_dist_zero_div_nat_le_one_div_nat (x : { x : ℝ // x ∈ Set.Icc 0 1 }) (n : ℕ) : dist 0 (↑x / ↑n) ≤ 1 / ↑n

Helper for Example 3.2.11: the distance from 0 to x/n is bounded by 1/n.

theorem uniformlyConvergent_x_div_nat_on_Icc_zero_one : UniformlyConvergent (fun (n : ℕ) (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => ↑x / ↑n) fun (x : { x : ℝ // x ∈ Set.Icc 0 1 }) => 0

Example 3.2.11: [Uniform convergence of x/n on [0,1]]. Let f_n(x) = x/n on [0,1] and f(x) = 0. Then f_n converges uniformly to f on [0,1].

theorem convergence_restrict_subset {X : Type u_1} {Y : Type u_2} [MetricSpace Y] (E : Set X) (f : ℕ → X → Y) (g : X → Y) : (PointwiseConvergent f g → PointwiseConvergent (fun (n : ℕ) (x : { x : X // x ∈ E }) => f n ↑x) fun (x : { x : X // x ∈ E }) => g ↑x) ∧ (UniformlyConvergent f g → UniformlyConvergent (fun (n : ℕ) (x : { x : X // x ∈ E }) => f n ↑x) fun (x : { x : X // x ∈ E }) => g ↑x)

Example 3.2.12: (i) pointwise convergence on X restricts to pointwise convergence on E; (ii) uniform convergence on X restricts to uniform convergence on E.