Grace/Cumulus/Metric/Structure.g17

Open in Workbench Download source

Imports

Maps · Topology.Spaces

Declarations

Source

1-- Bundled metric spaces: a space as one structure of its carrier and its2-- distance, the metric laws under their standard names, balls, the metric3-- topology as a space, convergence written u ⇝ x with its ε–N form, the4-- uniqueness of limits, and the metric rewrite set5-- 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.Structure11import Maps12import Topology.Spaces1314-- A metric space is a structure of its carrier and its distance, a15-- real-valued function on pairs of points written d(x, y) under a16-- hypothesis MetricSpace(X) and applied as X.dist(x, y) otherwise, built by17-- MetricSpace.mk(A, d) and read back by the projections X.carrier and18-- X.dist. MetricSpace(X) says that the distance is nonnegative, vanishes19-- exactly on the diagonal, is symmetric, and satisfies the triangle20-- inequality. IsMetric(A, d) remains the form over separate pieces, bridged21-- below.22structure MetricSpace23  | carrier : Set24  | dist : carrier × carrier → ℝ25  where26    dist_nonneg : ∀ x y ∈ carrier, relates(realLe, (0:R), dist(x, y))27    dist_eq_zero : ∀ x y ∈ carrier, dist(x, y) = (0:R) ↔ x = y28    dist_comm : ∀ x y ∈ carrier, dist(x, y) = dist(y, x)29    dist_triangle : ∀ x y z ∈ carrier,30      relates(realLe, dist(x, z), realAdd(dist(x, y), dist(y, z)))3132-- The projection laws of a constructed metric space as one rewrite set.33tactic metric_projections := simp [MetricSpace.mk.carrier, MetricSpace.mk.dist]3435-- Bridges between the structure and the form over separate pieces. The36-- bundled-to-unbundled direction is an instance, so `with *` reads the37-- metric off a space hypothesis.38instance MetricSpace.parts (X : Set)39  requires metric : MetricSpace(X)40  shows IsMetric(X.carrier, X.dist)41proof42  obtain ⟨shape, function, nonneg, zero, comm, triangle⟩ := metric43  unfold IsMetric44  exact ⟨function, nonneg, zero, comm, triangle⟩4546theorem MetricSpace.of_parts (A d : Set)47  requires metric : IsMetric(A, d)48  shows MetricSpace(MetricSpace.mk(A, d))49proof50  obtain ⟨function, nonneg, zero, comm, triangle⟩ := metric51  apply MetricSpace.intro52  . exact function53  . exact nonneg54  . exact zero55  . exact comm56  . exact triangle5758theorem MetricSpace.of_projections (X : Set)59  requires shape : MetricSpace.Data(X)60  requires metric : IsMetric(X.carrier, X.dist)61  shows MetricSpace(X)62proof63  obtain ⟨function, nonneg, zero, comm, triangle⟩ := metric64  unfold MetricSpace65  exact ⟨shape, function, nonneg, zero, comm, triangle⟩6667theorem MetricSpace.eta_of_space (X : Set)68  requires metric : MetricSpace(X)69  shows X = MetricSpace.mk(X.carrier, X.dist)70proof71  obtain ⟨shape, rest⟩ := metric72  exact MetricSpace.eta with shape7374-- The metric topology as a space: the open sets are those containing a75-- ball around each of their points. Its carrier is the carrier of X and76-- its open sets are metricTopology(A, d) over the pieces.77def metricTopology (X : Set) : Set :=78  TopologicalSpace.mk(MetricSpace.carrier(X),79    metricTopology(MetricSpace.carrier(X), MetricSpace.dist(X)))8081theorem metricTopology.carrier (X : Set)82  shows TopologicalSpace.carrier(metricTopology(X)) = MetricSpace.carrier(X)83proof84  unfold metricTopology85  topology_projections8687theorem metricTopology.opens (X : Set)88  shows TopologicalSpace.opens(metricTopology(X)) =89    metricTopology(MetricSpace.carrier(X), MetricSpace.dist(X))90proof91  unfold metricTopology92  topology_projections9394instance MetricSpace.topological_space (X : Set)95  requires metric : MetricSpace(X)96  shows TopologicalSpace(metricTopology(X))97proof98  have parts := MetricSpace.parts with metric99  unfold metricTopology100  exact TopologicalSpace.of_parts with (Open.metricTopology.topology with parts)101102instance MetricSpace.hausdorff (X : Set)103  requires metric : MetricSpace(X)104  shows Hausdorff(metricTopology(X))105proof106  have parts := MetricSpace.parts with metric107  unfold metricTopology108  exact Hausdorff.of_mk with (Open.metricTopology.hausdorff with parts)109110-- A sequence converging to a point of a metric space is written u ⇝ x: it111-- is convergence in the metric topology. Under a hypothesis MetricSpace(X)112-- a binder (x : X) is a set variable with x ∈ X.carrier.113notation infix 50 "⇝" => Converges(metricTopology(X), _, _) via hypothesis MetricSpace(X) for X.carrier114115-- The distance between two points is written d(x, y) wherever a hypothesis116-- in scope supplies the space; it is the value X.dist(x, y).117notation function "d(x, y)" => X.dist(x, y) via hypothesis MetricSpace(X) for X.carrier118119-- The open and closed balls. ball(A, d, x, r) and closedBall(A, d, x, r)120-- remain the forms over separate pieces.121def ball (X x : Set, r : Real) : Set :=122  ball(MetricSpace.carrier(X), MetricSpace.dist(X), x, r)123def closedBall (X x : Set, r : Real) : Set :=124  closedBall(MetricSpace.carrier(X), MetricSpace.dist(X), x, r)125126theorem ball.parts (X x : Set, r : Real)127  shows ball(X, x, r) = ball(MetricSpace.carrier(X), MetricSpace.dist(X), x, r)128proof129  simp [ball]130131theorem closedBall.parts (X x : Set, r : Real)132  shows closedBall(X, x, r) =133    closedBall(MetricSpace.carrier(X), MetricSpace.dist(X), x, r)134proof135  simp [closedBall]136137-- Under a hypothesis MetricSpace(X): Cauchy(X, u) says the terms of u are138-- eventually within any ε of each other, and Bounded(X, S) that the139-- distances within S have a bound. IsCauchy(A, d, u) and IsBounded(A, d, S)140-- remain the forms over separate pieces.141section Definitions142variable (X : Set)143hypothesis metric : MetricSpace(X)144145predicate Cauchy (u : Set) := IsCauchy(X.carrier, X.dist, u)146predicate Bounded (S : Set) := IsBounded(X.carrier, X.dist, S)147148end Definitions149150section MetricLaws151variable (X : Set)152hypothesis metric : MetricSpace(X)153154-- A distance is a real number; this is an instance, so the real155-- arithmetic and order on distances is synthesized.156instance dist_real (x y : X)157  shows d(x, y) ∈ ℝ158proof159  have parts := MetricSpace.parts with metric160  exact IsMetric.member_reals with parts, *161162theorem dist_nonneg (x y : X)163  shows (0:R) ≤ d(x, y)164proof165  have parts := MetricSpace.parts with metric166  exact IsMetric.nonnegative with parts, *167168theorem dist_self (x : X)169  shows d(x, x) = (0:R)170proof171  have parts := MetricSpace.parts with metric172  exact IsMetric.self with parts, *173174theorem dist_comm (x y : X)175  shows d(x, y) = d(y, x)176proof177  have parts := MetricSpace.parts with metric178  exact IsMetric.symmetric with parts, *179180theorem dist_triangle (x y z : X)181  shows d(x, z) ≤ d(x, y) + d(y, z)182proof183  have parts := MetricSpace.parts with metric184  exact IsMetric.triangle with parts, *185186theorem dist_eq_zero (x y : X)187  shows d(x, y) = (0:R) ↔ x = y188proof189  have parts := MetricSpace.parts with metric190  exact IsMetric.eq_zero_iff with parts, *191192theorem dist_pos (x y : X)193  shows (0:R) < d(x, y) ↔ x ≠ y194proof195  have parts := MetricSpace.parts with metric196  exact IsMetric.positive_iff_ne with parts, *197198theorem dist_triangle_left (x y z : X)199  shows d(y, z) ≤ d(x, y) + d(x, z)200proof201  have parts := MetricSpace.parts with metric202  exact IsMetric.triangle_from with parts, *203204theorem abs_dist_sub_le (x y z : X)205  shows abs(d(x, z) - d(y, z)) ≤ d(x, y)206proof207  have parts := MetricSpace.parts with metric208  exact IsMetric.abs_sub_le with parts, *209210-- Balls.211theorem mem_ball (x y : X) (r : Real)212  shows y ∈ ball(X, x, r) ↔ d(x, y) < r213proof214  have yIn : y ∈ X by assumption215  rw ball.parts216  have characterization := ball.membership at X.carrier, X.dist, x, r, y217  constructor218  . intro member219    have parts := characterization.forward with member220    exact parts.right221  . intro close222    exact characterization.backward with ⟨yIn, close⟩223224theorem mem_closedBall (x y : X) (r : Real)225  shows y ∈ closedBall(X, x, r) ↔ d(x, y) ≤ r226proof227  have yIn : y ∈ X by assumption228  rw closedBall.parts229  have characterization := closedBall.membership at X.carrier, X.dist, x, r, y230  constructor231  . intro member232    have parts := characterization.forward with member233    exact parts.right234  . intro close235    exact characterization.backward with ⟨yIn, close⟩236237theorem ball_subset (x : X) (r : Real)238  shows ball(X, x, r) ⊆ X239proof240  rw ball.parts241  exact Ball.ball.subset at X.carrier, X.dist, x, r242243theorem mem_ball_self (x : X) (r : Real)244  requires positive : 0 < r245  shows x ∈ ball(X, x, r)246proof247  have parts := MetricSpace.parts with metric248  rw ball.parts249  exact ball.center with parts, *250251theorem ball_mono (x : X) (r s : Real)252  requires radii : r ≤ s253  shows ball(X, x, r) ⊆ ball(X, x, s)254proof255  have parts := MetricSpace.parts with metric256  rw [ball.parts, ball.parts]257  exact Ball.ball.mono with parts, *258259theorem ball_subset_closedBall (x : X) (r : Real)260  shows ball(X, x, r) ⊆ closedBall(X, x, r)261proof262  have parts := MetricSpace.parts with metric263  rw [ball.parts, closedBall.parts]264  exact Ball.ball.subset_closedBall with parts, *265266-- The open sets of the metric topology: a set is open exactly when it267-- contains a ball around each of its points, and balls are open.268theorem Open.iff_balls (U : Set)269  requires hU : U ⊆ X270  shows Open(metricTopology(X), U) ↔271    ∀ x ∈ U, ∃ r ∈ ℝ, 0 < r ∧ ball(X, x, r) ⊆ U272proof273  have space := MetricSpace.topological_space with metric274  constructor275  . intros open x hx276    have member := Open.mem with open277    rw metricTopology.opens at member278    have inside := metricTopology.ball_inside with member, hx279    obtain ⟨r, hr, positive, small⟩ := inside280    witness r281    rw ball.parts282    exact ⟨hr, positive, small⟩283  . intro balls284    have engine : MetricOpen(X.carrier, X.dist, U)285      unfold MetricOpen286      refine ⟨hU, ?_⟩287      intros x hx288      obtain ⟨r, hr, positive, inside⟩ := balls with x, hx289      rw ball.parts at inside290      exact ⟨r, hr, positive, inside⟩291    have member : U ∈ TopologicalSpace.opens(metricTopology(X))292      rw metricTopology.opens293      exact metricTopology.of_open with engine294    exact Open.of_mem with space, member295296instance ball_open (x : X) (r : Real)297  shows Open(metricTopology(X), ball(X, x, r))298proof299  have parts := MetricSpace.parts with metric300  have space := MetricSpace.topological_space with metric301  have member : ball(X, x, r) ∈ TopologicalSpace.opens(metricTopology(X))302    rw [metricTopology.opens, ball.parts]303    exact ball.member_topology with parts, *304  exact Open.of_mem with space, member305306instance closedBall_closed (x : X) (r : Real)307  shows Closed(metricTopology(X), closedBall(X, x, r))308proof309  have parts := MetricSpace.parts with metric310  have closed := Closed.closedBall.closed with parts, *311  unfold MetricClosed at closed312  rw closedBall.parts313  unfold metricTopology314  exact Closed.of_mk with (Open.metricTopology.topology with parts), closed315316-- Convergence: u ⇝ x is convergence in the metric topology, which is the317-- ε–N form over the pieces and the textbook form on distances.318theorem Converges.iff_parts (u : Set) (x : X)319  requires sequence : u : ℕ → X.carrier320  shows u ⇝ x ↔ ConvergesIn(X.carrier, X.dist, u, x)321proof322  have parts := MetricSpace.parts with metric323  have space := MetricSpace.topological_space with metric324  have xIn : x ∈ X by assumption325  have sequenceIn : SequenceIn(X.carrier, u)326    unfold SequenceIn327    exact sequence328  have characterization := ConvergesIn.iff_open with parts, sequenceIn, xIn329  constructor330  . intro converges331    apply characterization.backward332    intros U open hxU333    have member : U ∈ TopologicalSpace.opens(metricTopology(X))334      rw metricTopology.opens335      exact metricTopology.of_open with open336    have openU := Open.of_mem with space, member337    exact Converges.eventually with converges, openU, hxU338  . intro converges339    have eventually : ∀ U, Open(metricTopology(X), U) → x ∈ U →340        ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → u(n) ∈ U341      intros U open hxU342      have member := Open.mem with open343      rw metricTopology.opens at member344      have metricOpen := metricTopology.open with member345      exact ConvergesIn.eventually_in_open with converges, metricOpen, hxU346    have sequenceT : u : ℕ → TopologicalSpace.carrier(metricTopology(X))347      rw metricTopology.carrier348      exact sequence349    have xInT : x ∈ TopologicalSpace.carrier(metricTopology(X))350      rw metricTopology.carrier351      exact xIn352    exact Converges.of_eventually with space, sequenceT, xInT, eventually353354theorem Converges.iff_dist (u : Set) (x : X)355  requires sequence : u : ℕ → X.carrier356  shows u ⇝ x ↔357    ∀ ε ∈ ℝ, 0 < ε →358      ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → d(x, u(n)) < ε359proof360  have bridge := Converges.iff_parts with *361  have xIn : x ∈ X by assumption362  have sequenceIn : SequenceIn(X.carrier, u)363    unfold SequenceIn364    exact sequence365  constructor366  . intro converges367    have engine := bridge.forward with converges368    obtain ⟨sequenceU, point, control⟩ := engine369    exact control370  . intro control371    apply bridge.backward372    unfold ConvergesIn373    exact ⟨sequenceIn, xIn, control⟩374375-- A sequence has at most one limit.376theorem Converges.unique_metric (u : Set) (x y : X)377  requires first : u ⇝ x378  requires second : u ⇝ y379  shows x = y380proof381  have space := MetricSpace.topological_space with metric382  have hausdorff := MetricSpace.hausdorff with metric383  exact Spaces.Converges.unique with space, hausdorff, first, second384385theorem Converges.cauchy (u : Set) (x : X)386  requires converges : u ⇝ x387  shows Cauchy(X, u)388proof389  have parts := MetricSpace.parts with metric390  have space := MetricSpace.topological_space with metric391  have sequence := Converges.sequence with space, converges392  rw metricTopology.carrier at sequence393  have bridge := Converges.iff_parts with sequence394  have engine := bridge.forward with converges395  unfold Cauchy396  exact ConvergesIn.cauchy with parts, engine397398theorem Converges.bounded_range (u : Set) (x : X)399  requires converges : u ⇝ x400  shows Bounded(X, functionImage(u, ℕ, X.carrier))401proof402  have parts := MetricSpace.parts with metric403  have space := MetricSpace.topological_space with metric404  have sequence := Converges.sequence with space, converges405  rw metricTopology.carrier at sequence406  have bridge := Converges.iff_parts with sequence407  have engine := bridge.forward with converges408  unfold Bounded409  exact ConvergesIn.range_bounded with parts, engine410411instance Cauchy.parts (u : Set)412  requires cauchy : Cauchy(X, u)413  shows IsCauchy(X.carrier, X.dist, u)414proof415  unfold Cauchy at cauchy416  exact cauchy417418theorem Cauchy.of_parts (u : Set)419  requires cauchy : IsCauchy(X.carrier, X.dist, u)420  shows Cauchy(X, u)421proof422  unfold Cauchy423  exact cauchy424425instance Bounded.parts (S : Set)426  requires bounded : Bounded(X, S)427  shows IsBounded(X.carrier, X.dist, S)428proof429  unfold Bounded at bounded430  exact bounded431432theorem Bounded.of_parts (S : Set)433  requires bounded : IsBounded(X.carrier, X.dist, S)434  shows Bounded(X, S)435proof436  unfold Bounded437  exact bounded438439instance ball_bounded (x : X) (r : Real)440  shows Bounded(X, ball(X, x, r))441proof442  have parts := MetricSpace.parts with metric443  unfold Bounded444  rw ball.parts445  exact Bounded.IsBounded.ball with parts, *446447theorem Cauchy.bounded_range (u : Set)448  requires cauchy : Cauchy(X, u)449  shows Bounded(X, functionImage(u, ℕ, X.carrier))450proof451  have parts := MetricSpace.parts with metric452  have pieces := Cauchy.parts with cauchy453  unfold Bounded454  exact Bounded.IsCauchy.range_bounded with parts, pieces455456end MetricLaws457458-- The metric rewrite set: the distance from a point to itself, the459-- vanishing criterion, and membership in balls.460tactic metric_simp := simp [dist_self, dist_eq_zero, mem_ball, mem_closedBall]461