Grace/Cumulus/Metric/Space.g17

Open in Workbench Download source

Imports

Real.Metric · Topology.Subspace

Declarations

Source

1-- Metric spaces: a distance function on a set with its defining laws and2-- their first consequences3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Metric.Space9import Real.Metric10import Topology.Subspace1112-- A metric on X is a real-valued function on X × X, applied as d(x, y),13-- that is nonnegative, vanishes exactly on the diagonal, is symmetric, and14-- satisfies the triangle inequality. Points of X are arbitrary sets, so the15-- real order and addition are written through their graphs here; once a16-- distance is known to be real, proofs use the usual notation.17predicate IsMetric (X d : Set) :=18  FunctionBetween(d, X × X, ℝ) ∧19  (∀ x ∈ X, ∀ y ∈ X, relates(realLe, (0:R), d(x, y))) ∧20  (∀ x ∈ X, ∀ y ∈ X, d(x, y) = (0:R) ↔ x = y) ∧21  (∀ x ∈ X, ∀ y ∈ X, d(x, y) = d(y, x)) ∧22  (∀ x ∈ X, ∀ y ∈ X, ∀ z ∈ X,23    relates(realLe, d(x, z), realAdd(d(x, y), d(y, z))))2425theorem IsMetric.function (X d : Set)26  requires metric : IsMetric(X, d)27  shows d : X × X → ℝ28proof29  exact metric.left3031theorem Metric.apply_pair (d x y : Set)32  shows d((x, y)) = d(x, y)33proof34  unfold call235  rfl3637theorem IsMetric.real (X d x y : Set)38  requires metric : IsMetric(X, d)39  requires hx : x ∈ X40  requires hy : y ∈ X41  shows Real(d(x, y))42proof43  have function := IsMetric.function with metric44  have pair := product.pair_membership.backward at x, y, X, X with ⟨hx, hy⟩45  unfold Real46  unfold call247  exact FunctionBetween.apply_closed with function, pair4849theorem IsMetric.member_reals (X d x y : Set)50  requires metric : IsMetric(X, d)51  requires hx : x ∈ X52  requires hy : y ∈ X53  shows d(x, y) ∈ ℝ54proof55  exact IsMetric.real with metric, hx, hy5657theorem IsMetric.nonnegative (X d x y : Set)58  requires metric : IsMetric(X, d)59  requires hx : x ∈ X60  requires hy : y ∈ X61  shows (0:R) ≤ d(x, y)62proof63  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric64  exact nonnegative with x, hx, y, hy6566theorem IsMetric.eq_zero_iff (X d x y : Set)67  requires metric : IsMetric(X, d)68  requires hx : x ∈ X69  requires hy : y ∈ X70  shows d(x, y) = (0:R) ↔ x = y71proof72  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric73  exact zero with x, hx, y, hy7475theorem IsMetric.self (X d x : Set)76  requires metric : IsMetric(X, d)77  requires hx : x ∈ X78  shows d(x, x) = (0:R)79proof80  have characterization := IsMetric.eq_zero_iff with metric, hx, hx81  apply characterization.backward82  rfl8384theorem IsMetric.eq_of_zero (X d x y : Set)85  requires metric : IsMetric(X, d)86  requires hx : x ∈ X87  requires hy : y ∈ X88  requires zero : d(x, y) = (0:R)89  shows x = y90proof91  have characterization := IsMetric.eq_zero_iff with metric, hx, hy92  exact characterization.forward with zero9394theorem IsMetric.symmetric (X d x y : Set)95  requires metric : IsMetric(X, d)96  requires hx : x ∈ X97  requires hy : y ∈ X98  shows d(x, y) = d(y, x)99proof100  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric101  exact symmetric with x, hx, y, hy102103theorem IsMetric.triangle (X d x y z : Set)104  requires metric : IsMetric(X, d)105  requires hx : x ∈ X106  requires hy : y ∈ X107  requires hz : z ∈ X108  shows d(x, z) ≤ realAdd(d(x, y), d(y, z))109proof110  obtain ⟨function, nonnegative, zero, symmetric, triangle⟩ := metric111  exact triangle with x, hx, y, hy, z, hz112113theorem IsMetric.positive_of_ne (X d x y : Set)114  requires metric : IsMetric(X, d)115  requires hx : x ∈ X116  requires hy : y ∈ X117  requires distinct : x ≠ y118  shows (0:R) < d(x, y)119proof120  have nonnegative := IsMetric.nonnegative with metric, hx, hy121  have real := IsMetric.real with metric, hx, hy122  have nonzero : d(x, y) ≠ 0123    intro zero124    exact distinct with (IsMetric.eq_of_zero with metric, hx, hy, zero)125  have order := realLess.trichotomy at (0:R), d(x, y)126  rcases order with positive | zero | negative127  . exact positive128  . exfalso129    symm at zero130    exact nonzero with zero131  . exfalso132    linarith133134theorem IsMetric.ne_of_positive (X d x y : Set)135  requires metric : IsMetric(X, d)136  requires hx : x ∈ X137  requires hy : y ∈ X138  requires positive : (0:R) < d(x, y)139  shows x ≠ y140proof141  intro same142  have zero : d(x, y) = (0:R)143    rw same144    exact IsMetric.self with metric, hy145  rw zero at positive146  exact realLess.not_self with positive147148theorem IsMetric.zero_or_positive (X d x y : Set)149  requires metric : IsMetric(X, d)150  requires hx : x ∈ X151  requires hy : y ∈ X152  shows x = y ∨ (0:R) < d(x, y)153proof154  have split : x = y ∨ x ≠ y by tauto155  cases split with same | distinct156  . left157    exact same158  . right159    exact IsMetric.positive_of_ne with metric, hx, hy, distinct160161theorem IsMetric.positive_iff_ne (X d x y : Set)162  requires metric : IsMetric(X, d)163  requires hx : x ∈ X164  requires hy : y ∈ X165  shows (0:R) < d(x, y) ↔ x ≠ y166proof167  constructor168  . intro positive169    exact IsMetric.ne_of_positive with metric, hx, hy, positive170  . intro distinct171    exact IsMetric.positive_of_ne with metric, hx, hy, distinct172173-- The triangle inequality with the middle point measured from the same174-- side, in the forms the ball lemmas use.175theorem IsMetric.triangle_from (X d x y z : Set)176  requires metric : IsMetric(X, d)177  requires hx : x ∈ X178  requires hy : y ∈ X179  requires hz : z ∈ X180  shows d(y, z) ≤ realAdd(d(x, y), d(x, z))181proof182  have triangle := IsMetric.triangle with metric, hy, hx, hz183  have symmetric := IsMetric.symmetric with metric, hy, hx184  rwa symmetric at triangle185186theorem IsMetric.triangle_to (X d x y z : Set)187  requires metric : IsMetric(X, d)188  requires hx : x ∈ X189  requires hy : y ∈ X190  requires hz : z ∈ X191  shows d(x, y) ≤ realAdd(d(x, z), d(y, z))192proof193  have triangle := IsMetric.triangle with metric, hx, hz, hy194  have symmetric := IsMetric.symmetric with metric, hz, hy195  rwa symmetric at triangle196197theorem IsMetric.sub_le (X d x y z : Set)198  requires metric : IsMetric(X, d)199  requires hx : x ∈ X200  requires hy : y ∈ X201  requires hz : z ∈ X202  shows realSubValue(d(x, z), d(y, z)) ≤ d(x, y)203proof204  have triangle := IsMetric.triangle with metric, hx, hy, hz205  have dxz := IsMetric.real with metric, hx, hz206  have dyz := IsMetric.real with metric, hy, hz207  have dxy := IsMetric.real with metric, hx, hy208  linarith209210-- The reverse triangle inequality: distances to a third point differ by at211-- most the distance between the two points.212theorem IsMetric.abs_sub_le (X d x y z : Set)213  requires metric : IsMetric(X, d)214  requires hx : x ∈ X215  requires hy : y ∈ X216  requires hz : z ∈ X217  shows abs(realSubValue(d(x, z), d(y, z))) ≤ d(x, y)218proof219  have dxz := IsMetric.real with metric, hx, hz220  have dyz := IsMetric.real with metric, hy, hz221  have dxy := IsMetric.real with metric, hx, hy222  have dyx := IsMetric.real with metric, hy, hx223  have forward := IsMetric.sub_le with metric, hx, hy, hz224  have backward := IsMetric.sub_le with metric, hy, hx, hz225  have symmetric := IsMetric.symmetric with metric, hx, hy226  have differenceReal : Real(d(x, z) - d(y, z)) by typecheck227  have sign := realLess.trichotomy at (0:R), d(x, z) - d(y, z)228  rcases sign with positive | zero | negative229  . have nonnegative : 0 ≤ d(x, z) - d(y, z) by linarith230    have unfolded := abs.of_nonnegative with nonnegative231    rw unfolded232    exact forward233  . have nonnegative : 0 ≤ d(x, z) - d(y, z) by linarith234    have unfolded := abs.of_nonnegative with nonnegative235    rw unfolded236    exact forward237  . have nonpositive : d(x, z) - d(y, z) ≤ 0 by linarith238    have unfolded := abs.of_nonpositive with nonpositive239    rw unfolded240    linarith241242theorem IsMetric.abs_sub_le_from (X d x y z : Set)243  requires metric : IsMetric(X, d)244  requires hx : x ∈ X245  requires hy : y ∈ X246  requires hz : z ∈ X247  shows abs(realSubValue(d(x, y), d(x, z))) ≤ d(y, z)248proof249  have bound := IsMetric.abs_sub_le with metric, hy, hz, hx250  have symmetricY := IsMetric.symmetric with metric, hy, hx251  have symmetricZ := IsMetric.symmetric with metric, hz, hx252  rwa [symmetricY, symmetricZ] at bound253254-- A path through two intermediate points.255theorem IsMetric.four_points (X d x y z w : Set)256  requires metric : IsMetric(X, d)257  requires hx : x ∈ X258  requires hy : y ∈ X259  requires hz : z ∈ X260  requires hw : w ∈ X261  shows d(x, y) ≤ realAdd(realAdd(d(x, z), d(z, w)), d(w, y))262proof263  have first := IsMetric.triangle with metric, hx, hz, hy264  have second := IsMetric.triangle with metric, hz, hw, hy265  have dxy := IsMetric.real with metric, hx, hy266  have dxz := IsMetric.real with metric, hx, hz267  have dzy := IsMetric.real with metric, hz, hy268  have dzw := IsMetric.real with metric, hz, hw269  have dwy := IsMetric.real with metric, hw, hy270  linarith271272theorem IsMetric.le_add_of_le (X d x y z : Set) (A B : Real)273  requires metric : IsMetric(X, d)274  requires hx : x ∈ X275  requires hy : y ∈ X276  requires hz : z ∈ X277  requires first : d(x, y) ≤ A278  requires second : d(y, z) ≤ B279  shows d(x, z) ≤ A + B280proof281  have triangle := IsMetric.triangle with metric, hx, hy, hz282  have dxy := IsMetric.real with metric, hx, hy283  have dyz := IsMetric.real with metric, hy, hz284  have dxz := IsMetric.real with metric, hx, hz285  linarith286287theorem IsMetric.lt_add_of_lt (X d x y z : Set) (A B : Real)288  requires metric : IsMetric(X, d)289  requires hx : x ∈ X290  requires hy : y ∈ X291  requires hz : z ∈ X292  requires first : d(x, y) < A293  requires second : d(y, z) < B294  shows d(x, z) < A + B295proof296  have triangle := IsMetric.triangle with metric, hx, hy, hz297  have dxy := IsMetric.real with metric, hx, hy298  have dyz := IsMetric.real with metric, hy, hz299  have dxz := IsMetric.real with metric, hx, hz300  linarith301302-- Two metrics on the same set agreeing at every pair of points coincide.303theorem IsMetric.ext (X d e : Set)304  requires metricD : IsMetric(X, d)305  requires metricE : IsMetric(X, e)306  requires same : ∀ x ∈ X, ∀ y ∈ X, d(x, y) = e(x, y)307  shows d = e308proof309  have functionD := IsMetric.function with metricD310  have functionE := IsMetric.function with metricE311  apply FunctionBetween.ext with functionD, functionE312  intros p hp313  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp314  rw shape315  have pairD := Metric.apply_pair at d, x, y316  have pairE := Metric.apply_pair at e, x, y317  rw [pairD, pairE]318  exact same with x, hx, y, hy319320-- The empty set carries the empty metric.321theorem IsMetric.empty322  shows IsMetric(∅, ∅)323proof324  have product := product.left_empty at ∅325  constructor326  . rw product327    exact FunctionBetween.empty at ℝ328  . constructor329    . intros x hx330      exfalso331      exact empty.membership with hx332    . constructor333      . intros x hx334        exfalso335        exact empty.membership with hx336      . constructor337        . intros x hx338          exfalso339          exact empty.membership with hx340        . intros x hx341          exfalso342          exact empty.membership with hx343