Grace/Cumulus/Metric/Limits.g17

Open in Workbench Download source

Imports

Product

Declarations

Source

1-- Limits in a metric space: convergence through open sets and through the2-- real sequence of distances to the limit, sequences agreeing eventually,3-- limits against closed balls, continuous images of convergent and Cauchy4-- sequences, and the closure of a set in metric terms5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Metric.Limits11import Product1213theorem SequenceIn.constant (X x : Set)14  requires hx : x ∈ X15  shows SequenceIn(X, constantFunction(ℕ, X, x))16proof17  exact constantFunction.function at ℕ, X, x with hx1819theorem IsCauchy.constant (X d x : Set)20  requires metric : IsMetric(X, d)21  requires hx : x ∈ X22  shows IsCauchy(X, d, constantFunction(ℕ, X, x))23proof24  have converges := constantFunction.converges_in with metric, hx25  exact ConvergesIn.cauchy with metric, converges2627-- Convergence through open neighbourhoods of the limit.28theorem ConvergesIn.iff_open (X d u x : Set)29  requires metric : IsMetric(X, d)30  requires sequence : SequenceIn(X, u)31  requires hx : x ∈ X32  shows ConvergesIn(X, d, u, x) ↔33    (∀ U, MetricOpen(X, d, U) → x ∈ U → ∃ N ∈ ℕ, ∀ n ∈ ℕ, (N ≤ n → u(n) ∈ U))34proof35  constructor36  . intro converges37    intros U open hxU38    exact ConvergesIn.eventually_in_open with converges, open, hxU39  . intro neighbourhoods40    apply ConvergesIn.of_eventually with sequence, hx41    intros ε hε positive42    have typedE : Real(ε) by exact hε43    have open := ball.open at X, d, x, ε with metric, hx44    have center := ball.center with metric, hx, positive45    obtain ⟨N, hN, inside⟩ := neighbourhoods with ball(X, d, x, ε), open, center46    refine ⟨N, hN, ?_⟩47    intros n hn le48    exact ball.distance with (inside with n, hn, le)4950-- Sequences that agree from some index on have the same limits.51theorem ConvergesIn.of_eventually_equal (X d u v x M : Set)52  requires converges : ConvergesIn(X, d, u, x)53  requires sequence : SequenceIn(X, v)54  requires hM : M ∈ ℕ55  requires agree : ∀ n ∈ ℕ, (M ≤ n → v(n) = u(n))56  shows ConvergesIn(X, d, v, x)57proof58  have hx := ConvergesIn.limit_point with converges59  apply ConvergesIn.of_eventually with sequence, hx60  intros ε hε positive61  obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive62  have natM : Nat(M) by exact hM63  have natN : Nat(N) by exact hN64  obtain ⟨K, hK, leM, leN⟩ := naturalPair.upper_bound at M, N65  refine ⟨K, hK, ?_⟩66  intros n hn le67  have natK : Nat(K) by exact hK68  have natn : Nat(n) by exact hn69  have aboveM := LessEqual.transitive with leM, le70  have aboveN := LessEqual.transitive with leN, le71  have same := agree with n, hn, aboveM72  rw same73  exact near with n, hn, aboveN7475theorem ConvergesIn.limit_in_closedBall (X d u x y : Set, r : Real)76  requires metric : IsMetric(X, d)77  requires converges : ConvergesIn(X, d, u, x)78  requires hy : y ∈ X79  requires terms : ∀ n ∈ ℕ, u(n) ∈ closedBall(X, d, y, r)80  shows x ∈ closedBall(X, d, y, r)81proof82  have closed := closedBall.closed at X, d, y, r with metric, hy83  exact ConvergesIn.limit_in_closed with closed, terms, converges8485theorem ConvergesIn.distance_le (X d u x y : Set, r : Real)86  requires metric : IsMetric(X, d)87  requires converges : ConvergesIn(X, d, u, x)88  requires hy : y ∈ X89  requires bounds : ∀ n ∈ ℕ, d(y, u(n)) ≤ r90  shows d(y, x) ≤ r91proof92  have sequence := ConvergesIn.sequence with converges93  have terms : ∀ n ∈ ℕ, u(n) ∈ closedBall(X, d, y, r)94    intros n hn95    have term := SequenceIn.term_of_member with sequence, hn96    exact closedBall.of_distance with term, (bounds with n, hn)97  have inBall := ConvergesIn.limit_in_closedBall with98    metric, converges, hy, terms99  exact closedBall.distance with inBall100101theorem ConvergesIn.map_continuous (f X d Y e u x : Set)102  requires continuous : IsMetricContinuous(f, X, d, Y, e)103  requires converges : ConvergesIn(X, d, u, x)104  shows ConvergesIn(Y, e, compose(f, u, ℕ, X, Y), f(x))105proof106  have hx := ConvergesIn.limit_point with converges107  have atX := IsMetricContinuous.at with continuous, hx108  exact ConvergesIn.map with atX, converges109110theorem IsLipschitz.cauchy (f X d Y e u : Set) (K : Real)111  requires metricD : IsMetric(X, d)112  requires metricE : IsMetric(Y, e)113  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)114  requires cauchy : IsCauchy(X, d, u)115  shows IsCauchy(Y, e, compose(f, u, ℕ, X, Y))116proof117  have uniform := IsLipschitz.uniformly_continuous with118    metricD, metricE, lipschitz119  exact IsUniformlyContinuous.cauchy with uniform, cauchy120121theorem IsIsometry.cauchy (f X d Y e u : Set)122  requires isometry : IsIsometry(f, X, d, Y, e)123  requires cauchy : IsCauchy(X, d, u)124  shows IsCauchy(Y, e, compose(f, u, ℕ, X, Y))125proof126  have uniform := IsIsometry.uniformly_continuous with isometry127  exact IsUniformlyContinuous.cauchy with uniform, cauchy128129theorem IsIsometry.converges (f X d Y e u x : Set)130  requires isometry : IsIsometry(f, X, d, Y, e)131  requires converges : ConvergesIn(X, d, u, x)132  shows ConvergesIn(Y, e, compose(f, u, ℕ, X, Y), f(x))133proof134  have continuous := IsIsometry.continuous with isometry135  exact ConvergesIn.map_continuous with continuous, converges136137-- The real sequence of distances to a point.138defgraph distanceSequence (X d u x : Set) (n ∈ ℕ) : ℝ := d(x, u(n))139requires metric : IsMetric(X, d)140requires sequence : SequenceIn(X, u)141requires hx : x ∈ X142proof143  have term := SequenceIn.term_of_member with sequence, member144  exact IsMetric.real with metric, hx, term145146theorem distanceSequence.real_sequence (X d u x : Set)147  requires metric : IsMetric(X, d)148  requires sequence : SequenceIn(X, u)149  requires hx : x ∈ X150  shows RealSequence(distanceSequence(X, d, u, x))151proof152  exact distanceSequence.function with metric, sequence, hx153154-- A sequence converges to x exactly when its distances to x tend to zero.155theorem ConvergesIn.distance_converges (X d u x : Set)156  requires metric : IsMetric(X, d)157  requires converges : ConvergesIn(X, d, u, x)158  shows ConvergesTo(distanceSequence(X, d, u, x), (0:R))159proof160  have sequence := ConvergesIn.sequence with converges161  have hx := ConvergesIn.limit_point with converges162  unfold ConvergesTo163  constructor164  . exact distanceSequence.real_sequence with metric, sequence, hx165  . intros E hE positive166    obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive167    refine ⟨N, hN, ?_⟩168    intros n hn le169    have term := SequenceIn.term_of_member with sequence, hn170    have distance := IsMetric.real with metric, hx, term171    have nonnegative := IsMetric.nonnegative with metric, hx, term172    have close := near with n, hn, le173    have value := distanceSequence.value at X, d, u, x, n with174      metric, sequence, hx175    rw value176    apply openBall.membership.backward177    refine ⟨distance, ?_⟩178    unfold dist179    have zero := realSubValue.zero_right at d(x, u(n))180    have unfolded := abs.of_nonnegative with nonnegative181    rw [zero, unfolded]182    exact close183184theorem ConvergesIn.of_distance_converges (X d u x : Set)185  requires metric : IsMetric(X, d)186  requires sequence : SequenceIn(X, u)187  requires hx : x ∈ X188  requires converges : ConvergesTo(distanceSequence(X, d, u, x), (0:R))189  shows ConvergesIn(X, d, u, x)190proof191  obtain ⟨realSequence, tail⟩ := converges192  apply ConvergesIn.of_eventually with sequence, hx193  intros ε hε positive194  obtain ⟨N, hN, near⟩ := tail with ε, hε, positive195  refine ⟨N, hN, ?_⟩196  intros n hn le197  have term := SequenceIn.term_of_member with sequence, hn198  have distance := IsMetric.real with metric, hx, term199  have nonnegative := IsMetric.nonnegative with metric, hx, term200  have inBall := near with n, hn, le201  have value := distanceSequence.value at X, d, u, x, n with202    metric, sequence, hx203  rw value at inBall204  obtain ⟨valueReal, close⟩ := openBall.membership.forward with inBall205  unfold dist at close206  have zero := realSubValue.zero_right at d(x, u(n))207  have unfolded := abs.of_nonnegative with nonnegative208  rw [zero, unfolded] at close209  exact close210211theorem ConvergesIn.iff_distance_converges (X d u x : Set)212  requires metric : IsMetric(X, d)213  requires sequence : SequenceIn(X, u)214  requires hx : x ∈ X215  shows216    ConvergesIn(X, d, u, x) ↔ ConvergesTo(distanceSequence(X, d, u, x), (0:R))217proof218  constructor219  . intro converges220    exact ConvergesIn.distance_converges with metric, converges221  . intro converges222    exact ConvergesIn.of_distance_converges with metric, sequence, hx, converges223224-- The closure in metric terms.225theorem metricClosure.closed (X d A : Set)226  requires metric : IsMetric(X, d)227  requires hA : A ⊆ X228  shows MetricClosed(X, d, closure(X, metricTopology(X, d), A))229proof230  exact closure.closed with (metricTopology.topology with metric), hA231232theorem metricClosure.contains (X d A : Set)233  requires metric : IsMetric(X, d)234  requires hA : A ⊆ X235  shows A ⊆ closure(X, metricTopology(X, d), A)236proof237  exact Grace.Cumulus.Topology.Space.closure.contains with238    (metricTopology.topology with metric), hA239240theorem metricClosure.subset (X d A : Set)241  requires metric : IsMetric(X, d)242  requires hA : A ⊆ X243  shows closure(X, metricTopology(X, d), A) ⊆ X244proof245  exact closure.subset with (metricTopology.topology with metric), hA246247theorem metricClosure.least (X d A C : Set)248  requires closed : MetricClosed(X, d, C)249  requires hAC : A ⊆ C250  shows closure(X, metricTopology(X, d), A) ⊆ C251proof252  unfold MetricClosed at closed253  exact closure.least with closed, hAC254255theorem metricClosure.of_closed (X d C : Set)256  requires metric : IsMetric(X, d)257  requires closed : MetricClosed(X, d, C)258  shows closure(X, metricTopology(X, d), C) = C259proof260  unfold MetricClosed at closed261  exact closure.of_closed with (metricTopology.topology with metric), closed262263theorem MetricClosed.iff_closure (X d C : Set)264  requires metric : IsMetric(X, d)265  requires hC : C ⊆ X266  shows MetricClosed(X, d, C) ↔ closure(X, metricTopology(X, d), C) = C267proof268  constructor269  . intro closed270    exact metricClosure.of_closed with metric, closed271  . intro equal272    have closed := metricClosure.closed with metric, hC273    rwa equal at closed274275-- The closure of a bounded set is bounded.276theorem IsBounded.closure (X d S : Set)277  requires metric : IsMetric(X, d)278  requires bounded : IsBounded(X, d, S)279  shows IsBounded(X, d, closure(X, metricTopology(X, d), S))280proof281  have inside := IsBounded.subset with bounded282  have split : Nonempty(S) ∨ ¬Nonempty(S) by tauto283  cases split with nonempty | empty284  . obtain ⟨x, hx⟩ := nonempty285    have hxX := inside with x, hx286    obtain ⟨r, hr, positive, ballInside⟩ :=287      IsBounded.ball_around with metric, bounded, hx288    have typedR : Real(r) by exact hr289    have closed := closedBall.closed at X, d, x, r with metric, hxX290    have closedInside := ball.subset_closedBall with metric, hxX291    have insideClosed := Subset.transitive with ballInside, closedInside292    have least := metricClosure.least with closed, insideClosed293    exact IsBounded.of_closedBall with metric, hxX, least294  . have equal : S = ∅295      apply Subset.antisymmetric296      . intros s hs297        exfalso298        apply empty299        exact ⟨s, hs⟩300      . exact empty.subset at S301    rw equal302    have closedEmpty := MetricClosed.empty at X, d with metric303    have same := metricClosure.of_closed with metric, closedEmpty304    rw same305    exact IsBounded.empty at X, d306307theorem MetricOpen.difference (X d U C : Set)308  requires metric : IsMetric(X, d)309  requires open : MetricOpen(X, d, U)310  requires closed : MetricClosed(X, d, C)311  shows MetricOpen(X, d, U ∖ C)312proof313  have openComplement := MetricClosed.complement_open with closed314  have both := MetricOpen.intersection2 with metric, open, openComplement315  have same : U ∖ C = U ∩ complement(X, C)316    have insideU := MetricOpen.subset with open317    ext y318    constructor319    . intro hy320      have parts := difference.membership.forward with hy321      apply intersection.membership.backward322      refine ⟨parts.left, ?_⟩323      exact complement.membership.backward with ⟨(insideU with324        y, parts.left), parts.right⟩325    . intro hy326      have parts := intersection.membership.forward with hy327      have away := complement.membership.forward with parts.right328      exact difference.membership.backward with ⟨parts.left, away.right⟩329  rwa same330331theorem MetricClosed.difference (X d C U : Set)332  requires metric : IsMetric(X, d)333  requires closed : MetricClosed(X, d, C)334  requires open : MetricOpen(X, d, U)335  shows MetricClosed(X, d, C ∖ U)336proof337  have closedComplement := MetricOpen.complement_closed with metric, open338  have both := MetricClosed.intersection2 with metric, closed, closedComplement339  have same : C ∖ U = C ∩ complement(X, U)340    have insideC := MetricClosed.subset with closed341    ext y342    constructor343    . intro hy344      have parts := difference.membership.forward with hy345      apply intersection.membership.backward346      refine ⟨parts.left, ?_⟩347      exact complement.membership.backward with ⟨(insideC with348        y, parts.left), parts.right⟩349    . intro hy350      have parts := intersection.membership.forward with hy351      have away := complement.membership.forward with parts.right352      exact difference.membership.backward with ⟨parts.left, away.right⟩353  rwa same354355theorem ball.subset_interior_closedBall (X d x : Set, r : Real)356  requires metric : IsMetric(X, d)357  requires hx : x ∈ X358  shows359    ball(X, d, x, r) ⊆ interiorIn(metricTopology(X, d), closedBall(X, d, x, r))360proof361  have open := ball.member_topology at X, d, x, r with metric, hx362  have inside := ball.subset_closedBall with metric, hx363  exact interiorIn.greatest with open, inside364365-- A point is isolated exactly when some ball around it is a singleton.366theorem metricTopology.singleton_open_iff (X d x : Set)367  requires metric : IsMetric(X, d)368  requires hx : x ∈ X369  shows MetricOpen(X, d, {x}) ↔ ∃ r ∈ ℝ, 0 < r ∧ ball(X, d, x, r) = {x}370proof371  constructor372  . intro open373    obtain ⟨r, hr, positive, inside⟩ :=374      MetricOpen.ball_inside with open, (singleton.self at x)375    refine ⟨r, hr, positive, ?_⟩376    apply Subset.antisymmetric377    . exact inside378    . intros y hy379      have same := singleton.membership.forward with hy380      rw same381      exact ball.center with metric, hx, positive382  . intro data383    obtain ⟨r, hr, positive, same⟩ := data384    constructor385    . intros y hy386      have equal := singleton.membership.forward with hy387      rwa equal388    . intros y hy389      have equal := singleton.membership.forward with hy390      rw under equal391      refine ⟨r, hr, positive, ?_⟩392      rw same393      exact Subset.reflexive at {x}394