Grace/Cumulus/Metric/Sequences.g17

Open in Workbench Download source

Imports

Continuity · Real.Analysis.SequentialCompactness

Declarations

Source

1-- Sequences in a metric space: convergence and its uniqueness, constant2-- sequences and subsequences, Cauchy sequences, their boundedness, and3-- complete spaces4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Metric.Sequences10import Continuity11import Real.Analysis.SequentialCompactness1213predicate SequenceIn (X u : Set) := FunctionBetween(u, ℕ, X)1415theorem SequenceIn.function (X u : Set)16  requires sequence : SequenceIn(X, u)17  shows u : ℕ → X18proof19  exact sequence2021theorem SequenceIn.term (X u : Set, n : Nat)22  requires sequence : SequenceIn(X, u)23  shows u(n) ∈ X24proof25  have function := SequenceIn.function with sequence26  have member : n ∈ ℕ by simp [Nat]27  exact FunctionBetween.apply_closed with function, member2829theorem SequenceIn.term_of_member (X u n : Set)30  requires sequence : SequenceIn(X, u)31  requires hn : n ∈ ℕ32  shows u(n) ∈ X33proof34  have function := SequenceIn.function with sequence35  exact FunctionBetween.apply_closed with function, hn3637theorem SequenceIn.compose (X Y u f : Set)38  requires sequence : SequenceIn(X, u)39  requires function : f : X → Y40  shows SequenceIn(Y, compose(f, u, ℕ, X, Y))41proof42  have uFunction := SequenceIn.function with sequence43  exact compose.function with uFunction, function4445theorem SequenceIn.subsequence (X u k : Set)46  requires sequence : SequenceIn(X, u)47  requires increasing : StrictlyIncreasingNat(k)48  shows SequenceIn(X, compose(u, k, ℕ, ℕ, X))49proof50  have uFunction := SequenceIn.function with sequence51  have selector := StrictlyIncreasingNat.function with increasing52  exact compose.function with selector, uFunction5354-- Two naturals have a common upper bound.55theorem naturalPair.upper_bound (M N : Nat)56  shows ∃ K ∈ ℕ, M ≤ K ∧ N ≤ K57proof58  have order := LessEqual.total at M, N59  cases order with le | ge60  . have member : N ∈ ℕ by simp [Nat]61    exact ⟨N, member, le, (LessEqual.reflexive at N)⟩62  . have member : M ∈ ℕ by simp [Nat]63    exact ⟨M, member, (LessEqual.reflexive at M), ge⟩6465-- Convergence6667predicate ConvergesIn (X d u x : Set) :=68  SequenceIn(X, u) ∧ x ∈ X ∧69  (∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → d(x, u(n)) < ε))7071theorem ConvergesIn.sequence (X d u x : Set)72  requires converges : ConvergesIn(X, d, u, x)73  shows SequenceIn(X, u)74proof75  exact converges.left7677theorem ConvergesIn.limit_point (X d u x : Set)78  requires converges : ConvergesIn(X, d, u, x)79  shows x ∈ X80proof81  obtain ⟨sequence, hx, tail⟩ := converges82  exact hx8384theorem ConvergesIn.eventually (X d u x : Set, ε : Real)85  requires converges : ConvergesIn(X, d, u, x)86  requires positive : 0 < ε87  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → d(x, u(n)) < ε)88proof89  obtain ⟨sequence, hx, tail⟩ := converges90  have realE : ε ∈ ℝ by typecheck91  exact tail with ε, realE, positive9293theorem ConvergesIn.of_eventually (X d u x : Set)94  requires sequence : SequenceIn(X, u)95  requires hx : x ∈ X96  requires tail : ∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → d(x, u(n)) < ε)97  shows ConvergesIn(X, d, u, x)98proof99  exact ⟨sequence, hx, tail⟩100101theorem ConvergesIn.eventually_ball (X d u x : Set, ε : Real)102  requires converges : ConvergesIn(X, d, u, x)103  requires positive : 0 < ε104  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → u(n) ∈ ball(X, d, x, ε))105proof106  have sequence := ConvergesIn.sequence with converges107  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive108  refine ⟨N, hN, ?_⟩109  intros n hn le110  have term := SequenceIn.term_of_member with sequence, hn111  exact ball.of_distance with term, (near with n, hn, le)112113theorem ConvergesIn.unique (X d u x y : Set)114  requires metric : IsMetric(X, d)115  requires first : ConvergesIn(X, d, u, x)116  requires second : ConvergesIn(X, d, u, y)117  shows x = y118proof119  have hx := ConvergesIn.limit_point with first120  have hy := ConvergesIn.limit_point with second121  have sequence := ConvergesIn.sequence with first122  by_contra123  have dxy := IsMetric.real with metric, hx, hy124  have halfPositive := ball.half_positive with metric, hx, hy, this125  have doubled := half.add_self at d(x, y)126  obtain ⟨M, hM, nearX⟩ := ConvergesIn.eventually with first, halfPositive127  obtain ⟨N, hN, nearY⟩ := ConvergesIn.eventually with second, halfPositive128  have natM : Nat(M) by exact hM129  have natN : Nat(N) by exact hN130  obtain ⟨K, hK, leM, leN⟩ := naturalPair.upper_bound at M, N131  have closeX := nearX with K, hK, leM132  have closeY := nearY with K, hK, leN133  have term := SequenceIn.term_of_member with sequence, hK134  have triangle := IsMetric.triangle with metric, hx, term, hy135  have symmetric := IsMetric.symmetric with metric, hy, term136  have dxu := IsMetric.real with metric, hx, term137  have duy := IsMetric.real with metric, term, hy138  have dyu := IsMetric.real with metric, hy, term139  linarith140141theorem constantFunction.converges_in (X d x : Set)142  requires metric : IsMetric(X, d)143  requires hx : x ∈ X144  shows ConvergesIn(X, d, constantFunction(ℕ, X, x), x)145proof146  have function := constantFunction.function at ℕ, X, x with hx147  have sequence : SequenceIn(X, constantFunction(ℕ, X, x)) by exact function148  apply ConvergesIn.of_eventually with sequence, hx149  intros ε hε positive150  have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with151    Naturals.constructor.zero152  refine ⟨0, zero, ?_⟩153  intros n hn le154  have value := constantFunction.apply with hn, hx155  rw value156  have self := IsMetric.self with metric, hx157  rw self158  exact positive159160theorem ConvergesIn.subsequence (X d u k x : Set)161  requires converges : ConvergesIn(X, d, u, x)162  requires increasing : StrictlyIncreasingNat(k)163  shows ConvergesIn(X, d, compose(u, k, ℕ, ℕ, X), x)164proof165  have sequence := ConvergesIn.sequence with converges166  have selector := StrictlyIncreasingNat.function with increasing167  have composite := SequenceIn.subsequence with sequence, increasing168  have hx := ConvergesIn.limit_point with converges169  apply ConvergesIn.of_eventually with composite, hx170  intros ε hε positive171  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive172  refine ⟨N, hN, ?_⟩173  intros n hn le174  have natN : Nat(N) by exact hN175  have natn : Nat(n) by exact hn176  have index := StrictlyIncreasingNat.index_le_value at k, n with increasing177  have image := FunctionBetween.apply_closed with selector, hn178  have natImage : Nat(k(n)) by exact image179  have beyond := LessEqual.transitive with le, index180  have uFunction := SequenceIn.function with sequence181  have value := compose.apply with selector, uFunction, hn182  rw value183  exact near with k(n), image, beyond184185-- A continuous map sends convergent sequences to convergent sequences.186theorem ConvergesIn.map (f X d Y e u x : Set)187  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)188  requires converges : ConvergesIn(X, d, u, x)189  shows ConvergesIn(Y, e, compose(f, u, ℕ, X, Y), f(x))190proof191  have function := MetricContinuousAt.function with continuous192  have sequence := ConvergesIn.sequence with converges193  have hx := ConvergesIn.limit_point with converges194  have composite := SequenceIn.compose with sequence, function195  have image := FunctionBetween.apply_closed with function, hx196  apply ConvergesIn.of_eventually with composite, image197  intros ε hε positive198  obtain ⟨δ, hδ, positiveD, maps⟩ :=199    MetricContinuousAt.control with continuous, positive200  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positiveD201  refine ⟨N, hN, ?_⟩202  intros n hn le203  have term := SequenceIn.term_of_member with sequence, hn204  have uFunction := SequenceIn.function with sequence205  have value := compose.apply with uFunction, function, hn206  rw value207  exact maps with u(n), term, (near with n, hn, le)208209theorem ConvergesIn.eventually_in_open (X d u x U : Set)210  requires converges : ConvergesIn(X, d, u, x)211  requires open : MetricOpen(X, d, U)212  requires hxU : x ∈ U213  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → u(n) ∈ U)214proof215  have sequence := ConvergesIn.sequence with converges216  obtain ⟨r, hr, positive, inside⟩ := MetricOpen.ball_inside with open, hxU217  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive218  refine ⟨N, hN, ?_⟩219  intros n hn le220  have term := SequenceIn.term_of_member with sequence, hn221  exact inside with u(n), (ball.of_distance with term, (near with n, hn, le))222223-- Limits of sequences in a closed set stay in the set.224theorem ConvergesIn.limit_in_closed (X d u x C : Set)225  requires closed : MetricClosed(X, d, C)226  requires terms : ∀ n ∈ ℕ, u(n) ∈ C227  requires converges : ConvergesIn(X, d, u, x)228  shows x ∈ C229proof230  have sequence := ConvergesIn.sequence with converges231  have hx := ConvergesIn.limit_point with converges232  apply MetricClosed.of_balls_meet with closed, hx233  intros r hr positive234  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive235  have natN : Nat(N) by exact hN236  have term := SequenceIn.term_of_member with sequence, hN237  have close := near with N, hN, (LessEqual.reflexive at N)238  witness u(N)239  apply intersection.membership.backward240  exact ⟨(ball.of_distance with term, close), (terms with N, hN)⟩241242theorem ConvergesIn.limit_in_closure (X d u x A : Set)243  requires metric : IsMetric(X, d)244  requires hA : A ⊆ X245  requires terms : ∀ n ∈ ℕ, u(n) ∈ A246  requires converges : ConvergesIn(X, d, u, x)247  shows x ∈ closure(X, metricTopology(X, d), A)248proof249  have sequence := ConvergesIn.sequence with converges250  have hx := ConvergesIn.limit_point with converges251  apply metricClosure.of_balls_meet with metric, hA, hx252  intros r hr positive253  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive254  have natN : Nat(N) by exact hN255  have term := SequenceIn.term_of_member with sequence, hN256  have close := near with N, hN, (LessEqual.reflexive at N)257  witness u(N)258  apply intersection.membership.backward259  exact ⟨(ball.of_distance with term, close), (terms with N, hN)⟩260261-- Cauchy sequences262263predicate IsCauchy (X d u : Set) :=264  SequenceIn(X, u) ∧265  (∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ m ∈ ℕ, ∀ n ∈ ℕ,266    (N ≤ m → N ≤ n → d(u(m), u(n)) < ε))267268theorem IsCauchy.sequence (X d u : Set)269  requires cauchy : IsCauchy(X, d, u)270  shows SequenceIn(X, u)271proof272  exact cauchy.left273274theorem IsCauchy.eventually (X d u : Set, ε : Real)275  requires cauchy : IsCauchy(X, d, u)276  requires positive : 0 < ε277  shows ∃ N ∈ ℕ, ∀ m ∈ ℕ, ∀ n ∈ ℕ, (N ≤ m → N ≤ n → d(u(m), u(n)) < ε)278proof279  obtain ⟨sequence, tail⟩ := cauchy280  have realE : ε ∈ ℝ by typecheck281  exact tail with ε, realE, positive282283theorem IsCauchy.of_eventually (X d u : Set)284  requires sequence : SequenceIn(X, u)285  requires tail : ∀ ε ∈ ℝ, 0 < ε → ∃ N ∈ ℕ, ∀ m ∈ ℕ, ∀ n ∈ ℕ,286    (N ≤ m → N ≤ n → d(u(m), u(n)) < ε)287  shows IsCauchy(X, d, u)288proof289  exact ⟨sequence, tail⟩290291theorem ConvergesIn.cauchy (X d u x : Set)292  requires metric : IsMetric(X, d)293  requires converges : ConvergesIn(X, d, u, x)294  shows IsCauchy(X, d, u)295proof296  have sequence := ConvergesIn.sequence with converges297  have hx := ConvergesIn.limit_point with converges298  apply IsCauchy.of_eventually with sequence299  intros ε hε positive300  have halfPositive := half.positive with positive301  have doubled := half.add_self at ε302  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, halfPositive303  refine ⟨N, hN, ?_⟩304  intros m hm n hn leM leN305  have termM := SequenceIn.term_of_member with sequence, hm306  have termN := SequenceIn.term_of_member with sequence, hn307  have closeM := near with m, hm, leM308  have closeN := near with n, hn, leN309  have triangle := IsMetric.triangle_from with metric, hx, termM, termN310  have dxm := IsMetric.real with metric, hx, termM311  have dxn := IsMetric.real with metric, hx, termN312  have dmn := IsMetric.real with metric, termM, termN313  linarith314315theorem IsCauchy.subsequence (X d u k : Set)316  requires cauchy : IsCauchy(X, d, u)317  requires increasing : StrictlyIncreasingNat(k)318  shows IsCauchy(X, d, compose(u, k, ℕ, ℕ, X))319proof320  have sequence := IsCauchy.sequence with cauchy321  have selector := StrictlyIncreasingNat.function with increasing322  have composite := SequenceIn.subsequence with sequence, increasing323  apply IsCauchy.of_eventually with composite324  intros ε hε positive325  obtain ⟨N, hN, near⟩ := IsCauchy.eventually with cauchy, positive326  refine ⟨N, hN, ?_⟩327  intros m hm n hn leM leN328  have natN : Nat(N) by exact hN329  have natM : Nat(m) by exact hm330  have natn : Nat(n) by exact hn331  have indexM := StrictlyIncreasingNat.index_le_value at k, m with increasing332  have indexN := StrictlyIncreasingNat.index_le_value at k, n with increasing333  have imageM := FunctionBetween.apply_closed with selector, hm334  have imageN := FunctionBetween.apply_closed with selector, hn335  have natImageM : Nat(k(m)) by exact imageM336  have natImageN : Nat(k(n)) by exact imageN337  have beyondM := LessEqual.transitive with leM, indexM338  have beyondN := LessEqual.transitive with leN, indexN339  have uFunction := SequenceIn.function with sequence340  have valueM := compose.apply with selector, uFunction, hm341  have valueN := compose.apply with selector, uFunction, hn342  rw [valueM, valueN]343  exact near with k(m), imageM, k(n), imageN, beyondM, beyondN344345-- A Cauchy sequence with a convergent subsequence converges.346theorem IsCauchy.converges_of_subsequence (X d u k x : Set)347  requires metric : IsMetric(X, d)348  requires cauchy : IsCauchy(X, d, u)349  requires increasing : StrictlyIncreasingNat(k)350  requires converges : ConvergesIn(X, d, compose(u, k, ℕ, ℕ, X), x)351  shows ConvergesIn(X, d, u, x)352proof353  have sequence := IsCauchy.sequence with cauchy354  have selector := StrictlyIncreasingNat.function with increasing355  have hx := ConvergesIn.limit_point with converges356  apply ConvergesIn.of_eventually with sequence, hx357  intros ε hε positive358  have halfPositive := half.positive with positive359  have doubled := half.add_self at ε360  obtain ⟨M, hM, close⟩ := IsCauchy.eventually with cauchy, halfPositive361  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, halfPositive362  have natM : Nat(M) by exact hM363  have natN : Nat(N) by exact hN364  obtain ⟨K, hK, leM, leN⟩ := naturalPair.upper_bound at M, N365  refine ⟨K, hK, ?_⟩366  intros n hn le367  have natK : Nat(K) by exact hK368  have natn : Nat(n) by exact hn369  have index := StrictlyIncreasingNat.index_le_value at k, n with increasing370  have image := FunctionBetween.apply_closed with selector, hn371  have natImage : Nat(k(n)) by exact image372  have aboveM := LessEqual.transitive with leM, le373  have aboveN := LessEqual.transitive with leN, le374  have imageAboveM := LessEqual.transitive with aboveM, index375  have imageAboveN := LessEqual.transitive with aboveN, index376  have uFunction := SequenceIn.function with sequence377  have value := compose.apply with selector, uFunction, hn378  have nearImage := near with n, hn, aboveN379  rw value at nearImage380  have closePair := close with k(n), image, n, hn, imageAboveM, aboveM381  have term := SequenceIn.term_of_member with sequence, hn382  have termImage := SequenceIn.term_of_member with sequence, image383  have triangle := IsMetric.triangle with metric, hx, termImage, term384  have dxi := IsMetric.real with metric, hx, termImage385  have din := IsMetric.real with metric, termImage, term386  have dxn := IsMetric.real with metric, hx, term387  linarith388389-- Finitely many initial terms stay within a bounded distance of the first.390theorem SequenceIn.prefix_bound (X d u : Set, N : Nat)391  requires metric : IsMetric(X, d)392  requires sequence : SequenceIn(X, u)393  shows ∃ B ∈ ℝ, 0 ≤ B ∧ ∀ n ∈ ℕ, (n ≤ N → d(u(0), u(n)) ≤ B)394proof395  induction N396  | zero =>397    have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with398      Naturals.constructor.zero399    have term := SequenceIn.term_of_member at X, u, 0 with sequence, zero400    have self := IsMetric.self at X, d, u(0) with metric, term401    have zeroReal : (0:R) ∈ ℝ by typecheck402    have reflexive : (0:R) ≤ 0 by linarith403    refine ⟨(0:R), zeroReal, reflexive, ?_⟩404    intros n hn le405    have natN : Nat(n) by exact hn406    have equal := LessEqual.antisymmetric with407      le, (Grace.Core.Nat.Order.LessEqual.zero at n)408    rw equal409    rw self410    exact reflexive411  | k + 1 using ih =>412    obtain ⟨B, hB, nonnegativeB, bound⟩ := ih413    have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with414      Naturals.constructor.zero415    have natNext : Nat(k + 1) by typecheck416    have next : k + 1 ∈ ℕ by exact nat.omega.forward with natNext417    have term0 := SequenceIn.term_of_member at X, u, 0 with sequence, zero418    have termNext := SequenceIn.term_of_member at X, u, k + 1 with419      sequence, next420    have distance := IsMetric.real at X, d, u(0), u(k + 1) with421      metric, term0, termNext422    have nonnegative := IsMetric.nonnegative at X, d, u(0), u(k + 1) with423      metric, term0, termNext424    have sumReal : B + d(u(0), u(k + 1)) ∈ ℝ by typecheck425    have sumNonnegative : (0:R) ≤ B + d(u(0), u(k + 1)) by linarith426    refine ⟨B + d(u(0), u(k + 1)), sumReal, sumNonnegative, ?_⟩427    intros n hn le428    have natN : Nat(n) by exact hn429    have order := Less.trichotomy at n, k + 1 with natN430    rcases order with below | equal | above431    . have le2 : n ≤ k by arith432      have earlier := bound with n, hn, le2433      have termN := SequenceIn.term_of_member at X, u, n with sequence, hn434      have distanceN := IsMetric.real at X, d, u(0), u(n) with435        metric, term0, termN436      linarith437    . rw equal438      linarith439    . exfalso440      have cycle : n < n by arith441      exact Less.irreflexive with cycle442443theorem IsCauchy.bounded (X d u : Set)444  requires metric : IsMetric(X, d)445  requires cauchy : IsCauchy(X, d, u)446  shows ∃ r ∈ ℝ, ∀ n ∈ ℕ, d(u(0), u(n)) < r447proof448  have sequence := IsCauchy.sequence with cauchy449  have one : (0:R) < 1 by linarith450  obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, one451  have natN : Nat(N) by exact hN452  obtain ⟨B, hB, nonnegativeB, bound⟩ :=453    SequenceIn.prefix_bound at X, d, u, N with454    metric, sequence455  have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with456    Naturals.constructor.zero457  have term0 := SequenceIn.term_of_member with sequence, zero458  have termN := SequenceIn.term_of_member with sequence, hN459  have d0N := IsMetric.real with metric, term0, termN460  have nonnegative := IsMetric.nonnegative with metric, term0, termN461  have radiusReal : B + d(u(0), u(N)) + 1 ∈ ℝ by typecheck462  refine ⟨B + d(u(0), u(N)) + 1, radiusReal, ?_⟩463  intros n hn464  have natn : Nat(n) by exact hn465  have termn := SequenceIn.term_of_member with sequence, hn466  have d0n := IsMetric.real with metric, term0, termn467  have order := LessEqual.total at n, N468  cases order with le | ge469  . have early := bound with n, hn, le470    linarith471  . have late := close with N, hN, n, hn, (LessEqual.reflexive at N), ge472    have dNn := IsMetric.real with metric, termN, termn473    have triangle := IsMetric.triangle with metric, term0, termN, termn474    linarith475476-- Complete spaces477478predicate IsComplete (X d : Set) :=479  IsMetric(X, d) ∧ (∀ u, IsCauchy(X, d, u) → ∃ x ∈ X, ConvergesIn(X, d, u, x))480481theorem IsComplete.metric (X d : Set)482  requires complete : IsComplete(X, d)483  shows IsMetric(X, d)484proof485  exact complete.left486487theorem IsComplete.limit (X d u : Set)488  requires complete : IsComplete(X, d)489  requires cauchy : IsCauchy(X, d, u)490  shows ∃ x ∈ X, ConvergesIn(X, d, u, x)491proof492  exact complete.right with u, cauchy493494theorem IsComplete.of_limits (X d : Set)495  requires metric : IsMetric(X, d)496  requires limits : ∀ u, IsCauchy(X, d, u) → ∃ x ∈ X, ConvergesIn(X, d, u, x)497  shows IsComplete(X, d)498proof499  exact ⟨metric, limits⟩500501-- In a complete space a Cauchy sequence converges exactly to the limit of502-- any convergent subsequence; conversely convergence is characterized by503-- the Cauchy property.504theorem IsComplete.cauchy_iff_converges (X d u : Set)505  requires complete : IsComplete(X, d)506  shows IsCauchy(X, d, u) ↔ ∃ x ∈ X, ConvergesIn(X, d, u, x)507proof508  have metric := IsComplete.metric with complete509  constructor510  . intro cauchy511    exact IsComplete.limit with complete, cauchy512  . intro data513    obtain ⟨x, hx, converges⟩ := data514    exact ConvergesIn.cauchy with metric, converges515