Grace/Cumulus/Metric/Bounded.g17

Open in Workbench Download source

Imports

Sequences

Declarations

Source

1-- Bounded sets in a metric space: sets of bounded diameter, balls and2-- finite unions, the range of a Cauchy sequence, and images under3-- Lipschitz maps4-- 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.Bounded10import Sequences1112predicate IsBounded (X d S : Set) :=13  (S ⊆ X) ∧ (∃ r ∈ ℝ, ∀ x ∈ S, ∀ y ∈ S, d(x, y) ≤ r)1415theorem IsBounded.subset (X d S : Set)16  requires bounded : IsBounded(X, d, S)17  shows S ⊆ X18proof19  exact bounded.left2021theorem IsBounded.bound (X d S : Set)22  requires bounded : IsBounded(X, d, S)23  shows ∃ r ∈ ℝ, ∀ x ∈ S, ∀ y ∈ S, d(x, y) ≤ r24proof25  exact bounded.right2627theorem IsBounded.of_bound (X d S : Set, r : Real)28  requires inside : S ⊆ X29  requires bound : ∀ x ∈ S, ∀ y ∈ S, d(x, y) ≤ r30  shows IsBounded(X, d, S)31proof32  have realR : r ∈ ℝ by typecheck33  exact ⟨inside, r, realR, bound⟩3435theorem IsBounded.empty (X d : Set)36  shows IsBounded(X, d, ∅)37proof38  apply IsBounded.of_bound at X, d, ∅, (0:R) with (empty.subset at X)39  intros x hx40  exfalso41  exact empty.membership with hx4243theorem IsBounded.singleton (X d x : Set)44  requires metric : IsMetric(X, d)45  requires hx : x ∈ X46  shows IsBounded(X, d, {x})47proof48  have inside : {x} ⊆ X49    intros z hz50    have same := singleton.membership.forward with hz51    rwa same52  apply IsBounded.of_bound at X, d, {x}, (0:R) with inside53  intros y hy z hz54  have sameY := singleton.membership.forward with hy55  have sameZ := singleton.membership.forward with hz56  rw [sameY, sameZ]57  have self := IsMetric.self with metric, hx58  rw self59  exact realLe.reflexive6061theorem IsBounded.of_subset (X d S T : Set)62  requires bounded : IsBounded(X, d, T)63  requires inside : S ⊆ T64  shows IsBounded(X, d, S)65proof66  obtain ⟨insideT, r, hr, bound⟩ := bounded67  refine ⟨(Subset.transitive with inside, insideT), r, hr, ?_⟩68  intros x hx y hy69  exact bound with x, (inside with x, hx), y, (inside with y, hy)7071theorem IsBounded.intersection2 (X d S T : Set)72  requires bounded : IsBounded(X, d, S)73  shows IsBounded(X, d, S ∩ T)74proof75  exact IsBounded.of_subset with bounded, (intersection.subset_left at S, T)7677theorem IsBounded.ball (X d x : Set, r : Real)78  requires metric : IsMetric(X, d)79  requires hx : x ∈ X80  shows IsBounded(X, d, ball(X, d, x, r))81proof82  apply IsBounded.of_bound at X, d, ball(X, d, x, r), r + r with83    (ball.subset at X, d, x, r)84  intros y hy z hz85  have hyX := ball.point with hy86  have hzX := ball.point with hz87  have nearY := ball.distance with hy88  have nearZ := ball.distance with hz89  have triangle := IsMetric.triangle_from with metric, hx, hyX, hzX90  have dxy := IsMetric.real with metric, hx, hyX91  have dxz := IsMetric.real with metric, hx, hzX92  have dyz := IsMetric.real with metric, hyX, hzX93  linarith9495theorem IsBounded.closedBall (X d x : Set, r : Real)96  requires metric : IsMetric(X, d)97  requires hx : x ∈ X98  shows IsBounded(X, d, closedBall(X, d, x, r))99proof100  apply IsBounded.of_bound at X, d, closedBall(X, d, x, r), r + r with101    (closedBall.subset at X, d, x, r)102  intros y hy z hz103  have hyX := closedBall.point with hy104  have hzX := closedBall.point with hz105  have nearY := closedBall.distance with hy106  have nearZ := closedBall.distance with hz107  have triangle := IsMetric.triangle_from with metric, hx, hyX, hzX108  have dxy := IsMetric.real with metric, hx, hyX109  have dxz := IsMetric.real with metric, hx, hzX110  have dyz := IsMetric.real with metric, hyX, hzX111  linarith112113theorem IsBounded.sphere (X d x : Set, r : Real)114  requires metric : IsMetric(X, d)115  requires hx : x ∈ X116  shows IsBounded(X, d, sphere(X, d, x, r))117proof118  have bounded := IsBounded.closedBall at X, d, x, r with metric, hx119  exact IsBounded.of_subset with bounded, (sphere.subset_closedBall with120    metric, hx)121122theorem IsBounded.of_ball (X d S x : Set, r : Real)123  requires metric : IsMetric(X, d)124  requires hx : x ∈ X125  requires inside : S ⊆ ball(X, d, x, r)126  shows IsBounded(X, d, S)127proof128  exact IsBounded.of_subset with (IsBounded.ball at X, d, x, r with129    metric, hx), inside130131theorem IsBounded.of_closedBall (X d S x : Set, r : Real)132  requires metric : IsMetric(X, d)133  requires hx : x ∈ X134  requires inside : S ⊆ closedBall(X, d, x, r)135  shows IsBounded(X, d, S)136proof137  exact IsBounded.of_subset with (IsBounded.closedBall at X, d, x, r with138    metric, hx), inside139140-- A nonempty bounded set lies in a ball around any of its points.141theorem IsBounded.ball_around (X d S x : Set)142  requires metric : IsMetric(X, d)143  requires bounded : IsBounded(X, d, S)144  requires hx : x ∈ S145  shows ∃ r ∈ ℝ, 0 < r ∧ S ⊆ ball(X, d, x, r)146proof147  obtain ⟨inside, r, hr, bound⟩ := bounded148  have hxX := inside with x, hx149  have self := IsMetric.self with metric, hxX150  have nonnegative : (0:R) ≤ r151    have selfBound := bound with x, hx, x, hx152    rw self at selfBound153    exact selfBound154  have radiusReal : r + 1 ∈ ℝ by typecheck155  have positive : (0:R) < r + 1 by linarith156  refine ⟨r + 1, radiusReal, positive, ?_⟩157  intros y hy158  have hyX := inside with y, hy159  have dxy := IsMetric.real with metric, hxX, hyX160  have near := bound with x, hx, y, hy161  apply ball.of_distance with hyX162  linarith163164theorem IsBounded.in_ball (X d S : Set)165  requires metric : IsMetric(X, d)166  requires bounded : IsBounded(X, d, S)167  requires nonempty : Nonempty(S)168  shows ∃ x ∈ X, ∃ r ∈ ℝ, 0 < r ∧ S ⊆ ball(X, d, x, r)169proof170  obtain ⟨x, hx⟩ := nonempty171  have hxX := IsBounded.subset with bounded, x, hx172  obtain ⟨r, hr, positive, inside⟩ :=173    IsBounded.ball_around with metric, bounded, hx174  exact ⟨x, hxX, r, hr, positive, inside⟩175176theorem IsBounded.iff_ball (X d S : Set)177  requires metric : IsMetric(X, d)178  requires nonempty : Nonempty(S)179  shows IsBounded(X, d, S) ↔ ∃ x ∈ X, ∃ r ∈ ℝ, S ⊆ ball(X, d, x, r)180proof181  constructor182  . intro bounded183    obtain ⟨x, hx, r, hr, positive, inside⟩ :=184      IsBounded.in_ball with metric, bounded, nonempty185    exact ⟨x, hx, r, hr, inside⟩186  . intro data187    obtain ⟨x, hx, r, hr, inside⟩ := data188    exact IsBounded.of_ball with metric, hx, inside189190theorem IsBounded.nonnegative_bound (X d S : Set)191  requires metric : IsMetric(X, d)192  requires bounded : IsBounded(X, d, S)193  shows ∃ r ∈ ℝ, 0 ≤ r ∧ ∀ x ∈ S, ∀ y ∈ S, d(x, y) ≤ r194proof195  obtain ⟨inside, r, hr, bound⟩ := bounded196  have split : Nonempty(S) ∨ ¬Nonempty(S) by tauto197  cases split with nonempty | empty198  . obtain ⟨x, hx⟩ := nonempty199    have hxX := inside with x, hx200    have self := IsMetric.self with metric, hxX201    have selfBound := bound with x, hx, x, hx202    rw self at selfBound203    exact ⟨r, hr, selfBound, bound⟩204  . have zeroReal : (0:R) ∈ ℝ by typecheck205    have reflexive : (0:R) ≤ 0 by linarith206    refine ⟨(0:R), zeroReal, reflexive, ?_⟩207    intros x hx208    exfalso209    apply empty210    exact ⟨x, hx⟩211212-- The union of two bounded sets is bounded.213theorem IsBounded.union2 (X d S T : Set)214  requires metric : IsMetric(X, d)215  requires boundedS : IsBounded(X, d, S)216  requires boundedT : IsBounded(X, d, T)217  shows IsBounded(X, d, S ∪ T)218proof219  have insideS := IsBounded.subset with boundedS220  have insideT := IsBounded.subset with boundedT221  have inside := union2.subset with insideS, insideT222  have splitS : Nonempty(S) ∨ ¬Nonempty(S) by tauto223  have splitT : Nonempty(T) ∨ ¬Nonempty(T) by tauto224  cases splitS with nonemptyS | emptyS225  . cases splitT with nonemptyT | emptyT226    . obtain ⟨s, hs⟩ := nonemptyS227      obtain ⟨t, ht⟩ := nonemptyT228      have hsX := insideS with s, hs229      have htX := insideT with t, ht230      obtain ⟨r, hr, positiveR, ballS⟩ :=231        IsBounded.ball_around with metric, boundedS, hs232      obtain ⟨q, hq, positiveQ, ballT⟩ :=233        IsBounded.ball_around with metric, boundedT, ht234      have dst := IsMetric.real with metric, hsX, htX235      apply IsBounded.of_bound at236        X, d, S ∪ T, (r + d(s, t) + q) + (r + d(s, t) + q) with237        inside238      have reach : ∀ x ∈ S ∪ T, d(s, x) ≤ r + d(s, t) + q239        intros x hx240        have hxX := inside with x, hx241        have dsx := IsMetric.real with metric, hsX, hxX242        have cases := union2.membership.forward with hx243        cases cases with inS | inT244        . have near := ball.distance with (ballS with x, inS)245          have nonnegative := IsMetric.nonnegative with metric, hsX, htX246          linarith247        . have near := ball.distance with (ballT with x, inT)248          have dtx := IsMetric.real with metric, htX, hxX249          have triangle := IsMetric.triangle with metric, hsX, htX, hxX250          linarith251      intros x hx y hy252      have hxX := inside with x, hx253      have hyX := inside with y, hy254      have reachX := reach with x, hx255      have reachY := reach with y, hy256      have triangle := IsMetric.triangle_from with metric, hsX, hxX, hyX257      have dsx := IsMetric.real with metric, hsX, hxX258      have dsy := IsMetric.real with metric, hsX, hyX259      have dxy := IsMetric.real with metric, hxX, hyX260      linarith261    . have equal : T = ∅262        apply Subset.antisymmetric263        . intros t ht264          exfalso265          apply emptyT266          exact ⟨t, ht⟩267        . exact empty.subset at T268      rw equal269      rw union2.right_empty270      exact boundedS271  . have equal : S = ∅272      apply Subset.antisymmetric273      . intros s hs274        exfalso275        apply emptyS276        exact ⟨s, hs⟩277      . exact empty.subset at S278    rw equal279    rw union2.left_empty280    exact boundedT281282theorem IsBounded.union_singleton (X d S x : Set)283  requires metric : IsMetric(X, d)284  requires bounded : IsBounded(X, d, S)285  requires hx : x ∈ X286  shows IsBounded(X, d, {x} ∪ S)287proof288  exact IsBounded.union2 with metric, (IsBounded.singleton with metric, hx),289    bounded290291theorem IsBounded.pair (X d x y : Set)292  requires metric : IsMetric(X, d)293  requires hx : x ∈ X294  requires hy : y ∈ X295  shows IsBounded(X, d, {x, y})296proof297  rw pair.eq_union2298  exact IsBounded.union2 with metric, (IsBounded.singleton with metric, hx),299    (IsBounded.singleton with metric, hy)300301-- The range of a Cauchy sequence is bounded.302theorem IsCauchy.range_bounded (X d u : Set)303  requires metric : IsMetric(X, d)304  requires cauchy : IsCauchy(X, d, u)305  shows IsBounded(X, d, functionImage(u, ℕ, X))306proof307  have sequence := IsCauchy.sequence with cauchy308  obtain ⟨r, hr, close⟩ := IsCauchy.bounded with metric, cauchy309  have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with310    Naturals.constructor.zero311  have term0 := SequenceIn.term_of_member with sequence, zero312  apply IsBounded.of_bound at X, d, functionImage(u, ℕ, X), r + r with313    (functionImage.subset at u, ℕ, X)314  intros x hx y hy315  obtain ⟨hxX, m, hm, shapeX⟩ := functionImage.membership.forward with hx316  obtain ⟨hyX, n, hn, shapeY⟩ := functionImage.membership.forward with hy317  have closeM := close with m, hm318  have closeN := close with n, hn319  rw ← shapeX at closeM320  rw ← shapeY at closeN321  have triangle := IsMetric.triangle_from with metric, term0, hxX, hyX322  have d0x := IsMetric.real with metric, term0, hxX323  have d0y := IsMetric.real with metric, term0, hyX324  have dxy := IsMetric.real with metric, hxX, hyX325  linarith326327theorem ConvergesIn.range_bounded (X d u x : Set)328  requires metric : IsMetric(X, d)329  requires converges : ConvergesIn(X, d, u, x)330  shows IsBounded(X, d, functionImage(u, ℕ, X))331proof332  have cauchy := ConvergesIn.cauchy with metric, converges333  exact IsCauchy.range_bounded with metric, cauchy334335-- Lipschitz maps send bounded sets to bounded sets.336theorem IsLipschitz.image_bounded (f X d Y e S : Set) (K : Real)337  requires metricD : IsMetric(X, d)338  requires metricE : IsMetric(Y, e)339  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)340  requires bounded : IsBounded(X, d, S)341  shows IsBounded(Y, e, functionImage(f, S, Y))342proof343  have function := IsLipschitz.function with lipschitz344  have nonnegative := IsLipschitz.nonnegative with lipschitz345  have inside := IsBounded.subset with bounded346  obtain ⟨r, hr, bound⟩ := IsBounded.bound with bounded347  apply IsBounded.of_bound at Y, e, functionImage(f, S, Y), K * r with348    (functionImage.subset at f, S, Y)349  intros v hv w hw350  obtain ⟨hvY, x, hx, shapeV⟩ := functionImage.membership.forward with hv351  obtain ⟨hwY, y, hy, shapeW⟩ := functionImage.membership.forward with hw352  rw [shapeV, shapeW]353  have hxX := inside with x, hx354  have hyX := inside with y, hy355  have estimate := IsLipschitz.bound with lipschitz, hxX, hyX356  have distance := bound with x, hx, y, hy357  have dxy := IsMetric.real with metricD, hxX, hyX358  have scaled := realLe.mul_left_of_nonnegative with distance, nonnegative359  have imageX := FunctionBetween.apply_closed with function, hxX360  have imageY := FunctionBetween.apply_closed with function, hyX361  have exy := IsMetric.real with metricE, imageX, imageY362  linarith363