Grace/Cumulus/Metric/Ball.g17

Open in Workbench Download source

Imports

Space

Declarations

Source

1-- Open balls, closed balls, and spheres in a metric space2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Metric.Ball8import Space910def ball (X d x : Set, r : Real) : Set :=11  { y ∈ X | relates(realLess, d(x, y), r) }1213theorem ball.subset (X d x : Set, r : Real)14  shows ball(X, d, x, r) ⊆ X15proof16  intros y hy17  have parts := ball.membership.forward with hy18  exact parts.left1920theorem ball.powerset (X d x : Set, r : Real)21  shows ball(X, d, x, r) ∈ 𝒫(X)22proof23  exact powerset.membership_iff.backward with (ball.subset at X, d, x, r)2425theorem ball.point (X d x y : Set, r : Real)26  requires member : y ∈ ball(X, d, x, r)27  shows y ∈ X28proof29  have parts := ball.membership.forward with member30  exact parts.left3132theorem ball.distance (X d x y : Set, r : Real)33  requires member : y ∈ ball(X, d, x, r)34  shows d(x, y) < r35proof36  have parts := ball.membership.forward with member37  exact parts.right3839theorem ball.of_distance (X d x y : Set, r : Real)40  requires hy : y ∈ X41  requires near : d(x, y) < r42  shows y ∈ ball(X, d, x, r)43proof44  exact ball.membership.backward with ⟨hy, near⟩4546theorem ball.center (X d x : Set, r : Real)47  requires metric : IsMetric(X, d)48  requires hx : x ∈ X49  requires positive : 0 < r50  shows x ∈ ball(X, d, x, r)51proof52  have self := IsMetric.self with metric, hx53  apply ball.of_distance with hx54  rw self55  exact positive5657theorem ball.nonempty (X d x : Set, r : Real)58  requires metric : IsMetric(X, d)59  requires hx : x ∈ X60  requires positive : 0 < r61  shows Nonempty(ball(X, d, x, r))62proof63  witness x64  exact ball.center with metric, hx, positive6566theorem ball.positive_of_member (X d x y : Set, r : Real)67  requires metric : IsMetric(X, d)68  requires hx : x ∈ X69  requires member : y ∈ ball(X, d, x, r)70  shows 0 < r71proof72  have hy := ball.point with member73  have near := ball.distance with member74  have nonnegative := IsMetric.nonnegative with metric, hx, hy75  have real := IsMetric.real with metric, hx, hy76  linarith7778theorem ball.empty_of_nonpositive (X d x : Set, r : Real)79  requires metric : IsMetric(X, d)80  requires hx : x ∈ X81  requires nonpositive : r ≤ 082  shows ball(X, d, x, r) = ∅83proof84  ext y85  constructor86  . intro hy87    have positive := ball.positive_of_member with metric, hx, hy88    exfalso89    linarith90  . intro hy91    exfalso92    exact empty.membership with hy9394theorem ball.symmetric_membership (X d x y : Set, r : Real)95  requires metric : IsMetric(X, d)96  requires hx : x ∈ X97  requires hy : y ∈ X98  shows y ∈ ball(X, d, x, r) ↔ x ∈ ball(X, d, y, r)99proof100  have symmetric := IsMetric.symmetric with metric, hx, hy101  constructor102  . intro member103    have near := ball.distance with member104    apply ball.of_distance with hx105    rwa symmetric at near106  . intro member107    have near := ball.distance with member108    apply ball.of_distance with hy109    rwa symmetric110111theorem ball.mono (X d x : Set, r s : Real)112  requires metric : IsMetric(X, d)113  requires hx : x ∈ X114  requires radii : r ≤ s115  shows ball(X, d, x, r) ⊆ ball(X, d, x, s)116proof117  intros y hy118  have point := ball.point with hy119  have near := ball.distance with hy120  have real := IsMetric.real with metric, hx, point121  apply ball.of_distance with point122  linarith123124theorem ball.mono_member (X d x y : Set, r s : Real)125  requires metric : IsMetric(X, d)126  requires hx : x ∈ X127  requires member : y ∈ ball(X, d, x, r)128  requires radii : r ≤ s129  shows y ∈ ball(X, d, x, s)130proof131  have inside := ball.mono with metric, hx, radii132  exact inside with y, member133134-- Stepping from the center of one ball into another adds the radii.135theorem ball.step (X d x y z : Set, r s : Real)136  requires metric : IsMetric(X, d)137  requires hx : x ∈ X138  requires first : y ∈ ball(X, d, x, r)139  requires second : z ∈ ball(X, d, y, s)140  shows z ∈ ball(X, d, x, r + s)141proof142  have hy := ball.point with first143  have hz := ball.point with second144  have nearY := ball.distance with first145  have nearZ := ball.distance with second146  have bound := IsMetric.lt_add_of_lt with metric, hx, hy, hz, nearY, nearZ147  exact ball.of_distance with hz, bound148149-- A ball around a point of a ball, with the remaining radius, stays inside.150theorem ball.inside_of_le (X d x y : Set, r s : Real)151  requires metric : IsMetric(X, d)152  requires hx : x ∈ X153  requires hy : y ∈ X154  requires room : realAdd(d(x, y), s) ≤ r155  shows ball(X, d, y, s) ⊆ ball(X, d, x, r)156proof157  intros z hz158  have point := ball.point with hz159  have near := ball.distance with hz160  have triangle := IsMetric.triangle with metric, hx, hy, point161  have dxy := IsMetric.real with metric, hx, hy162  have dyz := IsMetric.real with metric, hy, point163  have dxz := IsMetric.real with metric, hx, point164  apply ball.of_distance with point165  linarith166167theorem ball.inside (X d x y : Set, r : Real)168  requires metric : IsMetric(X, d)169  requires hx : x ∈ X170  requires member : y ∈ ball(X, d, x, r)171  shows ball(X, d, y, realSubValue(r, d(x, y))) ⊆ ball(X, d, x, r)172proof173  have hy := ball.point with member174  have dxy := IsMetric.real with metric, hx, hy175  have room : d(x, y) + (r - d(x, y)) ≤ r by linarith176  exact ball.inside_of_le with metric, hx, hy, room177178theorem ball.inside_radius_positive (X d x y : Set, r : Real)179  requires metric : IsMetric(X, d)180  requires hx : x ∈ X181  requires member : y ∈ ball(X, d, x, r)182  shows 0 < realSubValue(r, d(x, y))183proof184  have hy := ball.point with member185  have near := ball.distance with member186  have dxy := IsMetric.real with metric, hx, hy187  linarith188189-- Balls whose radii together do not reach the distance between the centers190-- are disjoint.191theorem ball.disjoint_of_separated (X d x y : Set, r s : Real)192  requires metric : IsMetric(X, d)193  requires hx : x ∈ X194  requires hy : y ∈ X195  requires separated : r + s ≤ d(x, y)196  shows Disjoint(ball(X, d, x, r), ball(X, d, y, s))197proof198  apply Disjoint.iff.backward199  intros z hzx hzy200  have point := ball.point with hzx201  have nearX := ball.distance with hzx202  have nearY := ball.distance with hzy203  have triangle := IsMetric.triangle_to with metric, hx, hy, point204  have dxy := IsMetric.real with metric, hx, hy205  have dxz := IsMetric.real with metric, hx, point206  have dyz := IsMetric.real with metric, hy, point207  linarith208209-- Distinct points have disjoint balls of half their distance.210theorem ball.half_disjoint (X d x y : Set)211  requires metric : IsMetric(X, d)212  requires hx : x ∈ X213  requires hy : y ∈ X214  requires distinct : x ≠ y215  shows Disjoint(ball(X, d, x, half(d(x, y))), ball(X, d, y, half(d(x, y))))216proof217  have dxy := IsMetric.real with metric, hx, hy218  have doubled := half.add_self at d(x, y)219  have separated : half(d(x, y)) + half(d(x, y)) ≤ d(x, y) by linarith220  exact ball.disjoint_of_separated with metric, hx, hy, separated221222theorem ball.half_positive (X d x y : Set)223  requires metric : IsMetric(X, d)224  requires hx : x ∈ X225  requires hy : y ∈ X226  requires distinct : x ≠ y227  shows 0 < half(d(x, y))228proof229  have positive := IsMetric.positive_of_ne with metric, hx, hy, distinct230  have dxy := IsMetric.real with metric, hx, hy231  exact half.positive with positive232233-- A point of two balls has a ball inside both.234theorem ball.common_radius (X d x y z : Set, r s : Real)235  requires metric : IsMetric(X, d)236  requires hx : x ∈ X237  requires hy : y ∈ X238  requires first : z ∈ ball(X, d, x, r)239  requires second : z ∈ ball(X, d, y, s)240  shows ∃ t ∈ ℝ, 0 < t ∧241    ball(X, d, z, t) ⊆ ball(X, d, x, r) ∧ ball(X, d, z, t) ⊆ ball(X, d, y, s)242proof243  have hz := ball.point with first244  have dxz := IsMetric.real with metric, hx, hz245  have dyz := IsMetric.real with metric, hy, hz246  have positiveX := ball.inside_radius_positive with metric, hx, first247  have positiveY := ball.inside_radius_positive with metric, hy, second248  have insideX := ball.inside with metric, hx, first249  have insideY := ball.inside with metric, hy, second250  have order := realLess.trichotomy at r - d(x, z), s - d(y, z)251  rcases order with smaller | equal | larger252  . have le := realLess.implies_le with smaller253    have realT : r - d(x, z) ∈ ℝ by typecheck254    refine ⟨r - d(x, z), realT, positiveX, insideX, ?_⟩255    have mono := ball.mono with metric, hz, le256    exact Subset.transitive with mono, insideY257  . have realT : r - d(x, z) ∈ ℝ by typecheck258    refine ⟨r - d(x, z), realT, positiveX, insideX, ?_⟩259    rw equal260    exact insideY261  . have le := realLess.implies_le with larger262    have realT : s - d(y, z) ∈ ℝ by typecheck263    refine ⟨s - d(y, z), realT, positiveY, ?_, insideY⟩264    have mono := ball.mono with metric, hz, le265    exact Subset.transitive with mono, insideX266267-- Closed balls268269def closedBall (X d x : Set, r : Real) : Set :=270  { y ∈ X | relates(realLe, d(x, y), r) }271272theorem closedBall.subset (X d x : Set, r : Real)273  shows closedBall(X, d, x, r) ⊆ X274proof275  intros y hy276  have parts := closedBall.membership.forward with hy277  exact parts.left278279theorem closedBall.point (X d x y : Set, r : Real)280  requires member : y ∈ closedBall(X, d, x, r)281  shows y ∈ X282proof283  have parts := closedBall.membership.forward with member284  exact parts.left285286theorem closedBall.distance (X d x y : Set, r : Real)287  requires member : y ∈ closedBall(X, d, x, r)288  shows d(x, y) ≤ r289proof290  have parts := closedBall.membership.forward with member291  exact parts.right292293theorem closedBall.of_distance (X d x y : Set, r : Real)294  requires hy : y ∈ X295  requires near : d(x, y) ≤ r296  shows y ∈ closedBall(X, d, x, r)297proof298  exact closedBall.membership.backward with ⟨hy, near⟩299300theorem closedBall.center (X d x : Set, r : Real)301  requires metric : IsMetric(X, d)302  requires hx : x ∈ X303  requires nonnegative : 0 ≤ r304  shows x ∈ closedBall(X, d, x, r)305proof306  have self := IsMetric.self with metric, hx307  apply closedBall.of_distance with hx308  rw self309  exact nonnegative310311theorem ball.subset_closedBall (X d x : Set, r : Real)312  requires metric : IsMetric(X, d)313  requires hx : x ∈ X314  shows ball(X, d, x, r) ⊆ closedBall(X, d, x, r)315proof316  intros y hy317  have point := ball.point with hy318  have near := ball.distance with hy319  have real := IsMetric.real with metric, hx, point320  apply closedBall.of_distance with point321  exact realLess.implies_le with near322323theorem closedBall.subset_ball (X d x : Set, r s : Real)324  requires metric : IsMetric(X, d)325  requires hx : x ∈ X326  requires radii : r < s327  shows closedBall(X, d, x, r) ⊆ ball(X, d, x, s)328proof329  intros y hy330  have point := closedBall.point with hy331  have near := closedBall.distance with hy332  have real := IsMetric.real with metric, hx, point333  apply ball.of_distance with point334  linarith335336theorem closedBall.mono (X d x : Set, r s : Real)337  requires metric : IsMetric(X, d)338  requires hx : x ∈ X339  requires radii : r ≤ s340  shows closedBall(X, d, x, r) ⊆ closedBall(X, d, x, s)341proof342  intros y hy343  have point := closedBall.point with hy344  have near := closedBall.distance with hy345  have real := IsMetric.real with metric, hx, point346  apply closedBall.of_distance with point347  linarith348349theorem closedBall.empty_of_negative (X d x : Set, r : Real)350  requires metric : IsMetric(X, d)351  requires hx : x ∈ X352  requires negative : r < 0353  shows closedBall(X, d, x, r) = ∅354proof355  ext y356  constructor357  . intro hy358    have point := closedBall.point with hy359    have near := closedBall.distance with hy360    have nonnegative := IsMetric.nonnegative with metric, hx, point361    have real := IsMetric.real with metric, hx, point362    exfalso363    linarith364  . intro hy365    exfalso366    exact empty.membership with hy367368theorem closedBall.zero (X d x : Set)369  requires metric : IsMetric(X, d)370  requires hx : x ∈ X371  shows closedBall(X, d, x, 0) = {x}372proof373  ext y374  constructor375  . intro hy376    have point := closedBall.point with hy377    have near := closedBall.distance with hy378    have nonnegative := IsMetric.nonnegative with metric, hx, point379    have real := IsMetric.real with metric, hx, point380    have zero : d(x, y) = (0:R) by linarith381    have same := IsMetric.eq_of_zero with metric, hx, point, zero382    rw same383    exact singleton.self at y384  . intro hy385    have same := singleton.membership.forward with hy386    rw same387    have reflexive : (0:R) ≤ 0 by linarith388    exact closedBall.center with metric, hx, reflexive389390theorem closedBall.symmetric_membership (X d x y : Set, r : Real)391  requires metric : IsMetric(X, d)392  requires hx : x ∈ X393  requires hy : y ∈ X394  shows y ∈ closedBall(X, d, x, r) ↔ x ∈ closedBall(X, d, y, r)395proof396  have symmetric := IsMetric.symmetric with metric, hx, hy397  constructor398  . intro member399    have near := closedBall.distance with member400    apply closedBall.of_distance with hx401    rwa symmetric at near402  . intro member403    have near := closedBall.distance with member404    apply closedBall.of_distance with hy405    rwa symmetric406407theorem closedBall.step (X d x y z : Set, r s : Real)408  requires metric : IsMetric(X, d)409  requires hx : x ∈ X410  requires first : y ∈ closedBall(X, d, x, r)411  requires second : z ∈ closedBall(X, d, y, s)412  shows z ∈ closedBall(X, d, x, r + s)413proof414  have hy := closedBall.point with first415  have hz := closedBall.point with second416  have nearY := closedBall.distance with first417  have nearZ := closedBall.distance with second418  have bound := IsMetric.le_add_of_le with metric, hx, hy, hz, nearY, nearZ419  exact closedBall.of_distance with hz, bound420421-- Spheres422423def sphere (X d x : Set, r : Real) : Set := { y ∈ X | d(x, y) = r }424425theorem sphere.subset (X d x : Set, r : Real)426  shows sphere(X, d, x, r) ⊆ X427proof428  intros y hy429  have parts := sphere.membership.forward with hy430  exact parts.left431432theorem sphere.subset_closedBall (X d x : Set, r : Real)433  requires metric : IsMetric(X, d)434  requires hx : x ∈ X435  shows sphere(X, d, x, r) ⊆ closedBall(X, d, x, r)436proof437  intros y hy438  obtain ⟨point, equal⟩ := sphere.membership.forward with hy439  have real := IsMetric.real with metric, hx, point440  apply closedBall.of_distance with point441  rw equal442  exact realLe.reflexive443444theorem sphere.disjoint_ball (X d x : Set, r : Real)445  shows Disjoint(sphere(X, d, x, r), ball(X, d, x, r))446proof447  apply Disjoint.iff.backward448  intros y onSphere inBall449  obtain ⟨point, equal⟩ := sphere.membership.forward with onSphere450  have near := ball.distance with inBall451  rw equal at near452  exact realLess.not_self with near453454theorem closedBall.eq_ball_union_sphere (X d x : Set, r : Real)455  requires metric : IsMetric(X, d)456  requires hx : x ∈ X457  shows closedBall(X, d, x, r) = ball(X, d, x, r) ∪ sphere(X, d, x, r)458proof459  apply Subset.antisymmetric460  . intros y hy461    have point := closedBall.point with hy462    have near := closedBall.distance with hy463    have real := IsMetric.real with metric, hx, point464    have order := realLess.trichotomy at d(x, y), r465    rcases order with less | equal | greater466    . exact union2.left with (ball.of_distance with point, less)467    . have onSphere : y ∈ sphere(X, d, x, r) := sphere.membership.backward with468      ⟨point, equal⟩469      exact union2.right with onSphere470    . exfalso471      linarith472  . apply union2.subset473    . exact ball.subset_closedBall with metric, hx474    . exact sphere.subset_closedBall with metric, hx475476theorem sphere.zero (X d x : Set)477  requires metric : IsMetric(X, d)478  requires hx : x ∈ X479  shows sphere(X, d, x, 0) = {x}480proof481  ext y482  constructor483  . intro hy484    obtain ⟨point, zero⟩ := sphere.membership.forward with hy485    have same := IsMetric.eq_of_zero with metric, hx, point, zero486    rw same487    exact singleton.self at y488  . intro hy489    have same := singleton.membership.forward with hy490    rw same491    have self := IsMetric.self with metric, hx492    exact sphere.membership.backward with ⟨hx, self⟩493494theorem sphere.empty_of_negative (X d x : Set, r : Real)495  requires metric : IsMetric(X, d)496  requires hx : x ∈ X497  requires negative : r < 0498  shows sphere(X, d, x, r) = ∅499proof500  ext y501  constructor502  . intro hy503    obtain ⟨point, equal⟩ := sphere.membership.forward with hy504    have nonnegative := IsMetric.nonnegative with metric, hx, point505    rw equal at nonnegative506    exfalso507    linarith508  . intro hy509    exfalso510    exact empty.membership with hy511