Grace/Cumulus/Metric/Spaces.g17

Open in Workbench Download source

Imports

Structure

Declarations

Source

1-- Maps between metric spaces and metric spaces built from others:2-- ε–δ continuity against continuity of the metric topologies, Lipschitz3-- maps, isometries, and uniform continuity, completeness, and the real4-- line, discrete, subspace, and product metrics as values5-- 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.Spaces11import Structure1213-- MetricContinuous(f, X, Y): f is an ε–δ continuous function between the14-- carriers; Lipschitz(f, X, Y, K), Isometry(f, X, Y), and15-- UniformlyContinuous(f, X, Y) likewise, and Complete(X) says every Cauchy16-- sequence converges. Each takes the spaces, so a hypothesis supplies both17-- distances. IsMetricContinuous(f, A, d, B, e) and the rest remain the forms18-- over separate pieces, bridged below.19predicate MetricContinuous (f X Y : Set) :=20  MetricSpace(X) ∧ MetricSpace(Y) ∧21  IsMetricContinuous(f, X.carrier, X.dist, Y.carrier, Y.dist)22predicate Lipschitz (f X Y : Set) (K : Real) :=23  MetricSpace(X) ∧ MetricSpace(Y) ∧24  IsLipschitz(f, X.carrier, X.dist, Y.carrier, Y.dist, K)25predicate Isometry (f X Y : Set) :=26  MetricSpace(X) ∧ MetricSpace(Y) ∧27  IsIsometry(f, X.carrier, X.dist, Y.carrier, Y.dist)28predicate UniformlyContinuous (f X Y : Set) :=29  MetricSpace(X) ∧ MetricSpace(Y) ∧30  IsUniformlyContinuous(f, X.carrier, X.dist, Y.carrier, Y.dist)31predicate Complete (X : Set) :=32  IsComplete(MetricSpace.carrier(X), MetricSpace.dist(X))3334-- A continuity, isometry, or Lipschitz hypothesis supplies convergence in35-- both of its spaces, so under it the binders (x : X) and (y : Y) are36-- carrier memberships and u ⇝ x is read in the space of its limit.37notation infix 50 "⇝" => Converges(metricTopology(X), _, _) via hypothesis MetricContinuous(f, X, Y) for X.carrier38notation infix 50 "⇝" => Converges(metricTopology(Y), _, _) via hypothesis MetricContinuous(f, X, Y) for Y.carrier39notation infix 50 "⇝" => Converges(metricTopology(X), _, _) via hypothesis Isometry(f, X, Y) for X.carrier40notation infix 50 "⇝" => Converges(metricTopology(Y), _, _) via hypothesis Isometry(f, X, Y) for Y.carrier41notation infix 50 "⇝" => Converges(metricTopology(X), _, _) via hypothesis Lipschitz(f, X, Y, K) for X.carrier42notation infix 50 "⇝" => Converges(metricTopology(Y), _, _) via hypothesis Lipschitz(f, X, Y, K) for Y.carrier43notation function "d(x, y)" => X.dist(x, y) via hypothesis MetricContinuous(f, X, Y) for X.carrier44notation function "d(x, y)" => Y.dist(x, y) via hypothesis MetricContinuous(f, X, Y) for Y.carrier45notation function "d(x, y)" => X.dist(x, y) via hypothesis Isometry(f, X, Y) for X.carrier46notation function "d(x, y)" => Y.dist(x, y) via hypothesis Isometry(f, X, Y) for Y.carrier47notation function "d(x, y)" => X.dist(x, y) via hypothesis Lipschitz(f, X, Y, K) for X.carrier48notation function "d(x, y)" => Y.dist(x, y) via hypothesis Lipschitz(f, X, Y, K) for Y.carrier4950instance MetricContinuous.parts (f X Y : Set)51  requires continuous : MetricContinuous(f, X, Y)52  shows IsMetricContinuous(f, X.carrier, X.dist, Y.carrier, Y.dist)53proof54  obtain ⟨metricX, metricY, engine⟩ := continuous55  exact engine5657theorem MetricContinuous.of_projections (f X Y : Set)58  requires metricX : MetricSpace(X)59  requires metricY : MetricSpace(Y)60  requires continuous :61    IsMetricContinuous(f, X.carrier, X.dist, Y.carrier, Y.dist)62  shows MetricContinuous(f, X, Y)63proof64  unfold MetricContinuous65  exact ⟨metricX, metricY, continuous⟩6667theorem MetricContinuous.source (f X Y : Set)68  requires continuous : MetricContinuous(f, X, Y)69  shows MetricSpace(X)70proof71  obtain ⟨metricX, rest⟩ := continuous72  exact metricX7374theorem MetricContinuous.target (f X Y : Set)75  requires continuous : MetricContinuous(f, X, Y)76  shows MetricSpace(Y)77proof78  obtain ⟨metricX, metricY, rest⟩ := continuous79  exact metricY8081theorem MetricContinuous.function_between (f X Y : Set)82  requires continuous : MetricContinuous(f, X, Y)83  shows f : X.carrier → Y.carrier84proof85  have engine := MetricContinuous.parts with continuous86  exact Continuity.IsMetricContinuous.function with engine8788-- ε–δ continuity is continuity of the metric topologies.89theorem MetricContinuous.iff_continuous (f X Y : Set)90  requires metricX : MetricSpace(X)91  requires metricY : MetricSpace(Y)92  shows MetricContinuous(f, X, Y) ↔93    f : metricTopology(X) ⇒ metricTopology(Y)94proof95  have partsX := MetricSpace.parts with metricX96  have partsY := MetricSpace.parts with metricY97  have spaceX := MetricSpace.topological_space with metricX98  have spaceY := MetricSpace.topological_space with metricY99  have criterion := IsMetricContinuous.iff_continuous_map at f, X.carrier, X.dist, Y.carrier, Y.dist with partsX, partsY100  constructor101  . intro continuous102    have engine := MetricContinuous.parts with continuous103    have map := criterion.forward with engine104    have shifted : ContinuousMap(f, TopologicalSpace.carrier(metricTopology(X)),105        TopologicalSpace.opens(metricTopology(X)),106        TopologicalSpace.carrier(metricTopology(Y)),107        TopologicalSpace.opens(metricTopology(Y)))108      rw [metricTopology.carrier, metricTopology.opens]109      rw [metricTopology.carrier, metricTopology.opens]110      exact map111    exact Continuous.of_projections with spaceX, spaceY, shifted112  . intro continuous113    have map := Continuous.parts with continuous114    rw [metricTopology.carrier, metricTopology.opens] at map115    rw [metricTopology.carrier, metricTopology.opens] at map116    have engine := criterion.backward with map117    exact MetricContinuous.of_projections with metricX, metricY, engine118119theorem MetricContinuous.continuous (f X Y : Set)120  requires continuous : MetricContinuous(f, X, Y)121  shows f : metricTopology(X) ⇒ metricTopology(Y)122proof123  have metricX := MetricContinuous.source with continuous124  have metricY := MetricContinuous.target with continuous125  have criterion := MetricContinuous.iff_continuous at f, X, Y with metricX, metricY126  exact criterion.forward with continuous127128section ContinuityLaws129variable (f X Y : Set)130hypothesis continuous : MetricContinuous(f, X, Y)131132theorem MetricContinuous.apply_mem (x : X)133  shows f(x) ∈ Y134proof135  have function := MetricContinuous.function_between with continuous136  have xIn : x ∈ X by assumption137  exact FunctionBetween.apply_closed with function, xIn138139-- The ε–δ form at a point.140theorem MetricContinuous.control (x : X) (ε : Real)141  requires positive : 0 < ε142  shows ∃ δ ∈ ℝ, 0 < δ ∧143    ∀ y ∈ X, (d(x, y) < δ → d(f(x), f(y)) < ε)144proof145  have engine := MetricContinuous.parts with continuous146  have xIn : x ∈ X by assumption147  have pointwise := Continuity.IsMetricContinuous.at with engine, xIn148  exact MetricContinuousAt.control with pointwise, positive149150-- A continuous map carries a convergent sequence to a convergent sequence.151theorem MetricContinuous.map_converges (u : Set) (x : X)152  requires converges : u ⇝ x153  shows compose(f, u, ℕ, X.carrier, Y.carrier) ⇝ f(x)154proof155  have metricX := MetricContinuous.source with continuous156  have metricY := MetricContinuous.target with continuous157  have spaceX := MetricSpace.topological_space with metricX158  have engine := MetricContinuous.parts with continuous159  have function := MetricContinuous.function_between with continuous160  have xIn : x ∈ X by assumption161  have image := FunctionBetween.apply_closed with function, xIn162  have sequence := Converges.sequence with spaceX, converges163  rw metricTopology.carrier at sequence164  have composite := compose.function with sequence, function165  have bridge := Converges.iff_parts with metricX, sequence166  have limit := bridge.forward with converges167  have mapped := ConvergesIn.map_continuous with engine, limit168  have bridgeY := Converges.iff_parts with metricY, composite169  exact bridgeY.backward with mapped170171end ContinuityLaws172173theorem MetricContinuous.id (X : Set)174  requires metric : MetricSpace(X)175  shows MetricContinuous(identity(X.carrier), X, X)176proof177  have parts := MetricSpace.parts with metric178  have engine := identity.metric_continuous at X.carrier, X.dist179  exact MetricContinuous.of_projections with *180181theorem MetricContinuous.comp (f g X Y Z : Set)182  requires first : MetricContinuous(f, X, Y)183  requires second : MetricContinuous(g, Y, Z)184  shows MetricContinuous(compose(g, f, X.carrier, Y.carrier, Z.carrier), X, Z)185proof186  have engineF := MetricContinuous.parts with first187  have engineG := MetricContinuous.parts with second188  have metricX := MetricContinuous.source with first189  have metricZ := MetricContinuous.target with second190  have engine := Continuity.IsMetricContinuous.compose with engineF, engineG191  exact MetricContinuous.of_projections with *192193-- Lipschitz maps, isometries, and uniformly continuous maps are194-- continuous; an isometry preserves distances.195theorem Lipschitz.metric_continuous (f X Y : Set) (K : Real)196  requires lipschitz : Lipschitz(f, X, Y, K)197  shows MetricContinuous(f, X, Y)198proof199  obtain ⟨metricX, metricY, engine⟩ := lipschitz200  have partsX := MetricSpace.parts with metricX201  have partsY := MetricSpace.parts with metricY202  have continuous := Continuity.IsLipschitz.continuous with partsX, partsY,203    engine204  exact MetricContinuous.of_projections with *205206theorem Isometry.metric_continuous (f X Y : Set)207  requires isometry : Isometry(f, X, Y)208  shows MetricContinuous(f, X, Y)209proof210  obtain ⟨metricX, metricY, engine⟩ := isometry211  have continuous := Continuity.IsIsometry.continuous with engine212  exact MetricContinuous.of_projections with *213214theorem UniformlyContinuous.metric_continuous (f X Y : Set)215  requires uniform : UniformlyContinuous(f, X, Y)216  shows MetricContinuous(f, X, Y)217proof218  obtain ⟨metricX, metricY, engine⟩ := uniform219  have continuous := Uniform.IsUniformlyContinuous.continuous with engine220  exact MetricContinuous.of_projections with *221222section IsometryLaws223variable (f X Y : Set)224hypothesis isometry : Isometry(f, X, Y)225226theorem Isometry.dist (x y : X)227  shows d(f(x), f(y)) = d(x, y)228proof229  obtain ⟨metricX, metricY, engine⟩ := isometry230  have xIn : x ∈ X by assumption231  have yIn : y ∈ X by assumption232  exact IsIsometry.distance with engine, xIn, yIn233234end IsometryLaws235236section LipschitzLaws237variable (f X Y : Set) (K : Real)238hypothesis lipschitz : Lipschitz(f, X, Y, K)239240theorem Lipschitz.dist_le (x y : X)241  shows d(f(x), f(y)) ≤ K * d(x, y)242proof243  obtain ⟨metricX, metricY, engine⟩ := lipschitz244  have xIn : x ∈ X by assumption245  have yIn : y ∈ X by assumption246  exact IsLipschitz.bound with engine, xIn, yIn247248end LipschitzLaws249250-- Completeness.251instance Complete.parts (X : Set)252  requires complete : Complete(X)253  shows IsComplete(MetricSpace.carrier(X), MetricSpace.dist(X))254proof255  unfold Complete at complete256  exact complete257258theorem Complete.of_parts (X : Set)259  requires complete : IsComplete(MetricSpace.carrier(X), MetricSpace.dist(X))260  shows Complete(X)261proof262  unfold Complete263  exact complete264265theorem Complete.of_mk (A d : Set)266  requires complete : IsComplete(A, d)267  shows Complete(MetricSpace.mk(A, d))268proof269  unfold Complete270  metric_projections271272theorem Complete.converges (X u : Set)273  requires metric : MetricSpace(X)274  requires complete : Complete(X)275  requires cauchy : Cauchy(X, u)276  shows ∃ x ∈ X, u ⇝ x277proof278  have pieces := Complete.parts with complete279  have cauchyU := Cauchy.parts with cauchy280  have limit := Sequences.IsComplete.limit with pieces, cauchyU281  obtain ⟨x, xIn, converges⟩ := limit282  have sequence := SequenceIn.function with (IsCauchy.sequence with cauchyU)283  have bridge := Converges.iff_parts at X, u, x with metric, sequence284  witness x285  exact ⟨xIn, (bridge.backward with converges)⟩286287-- The real line with its usual distance, the discrete metric on a set, the288-- subspace metric on a subset, and the product of two metric spaces.289def realMetric : Set := MetricSpace.mk(ℝ, realDistance)290def discreteMetric (A : Set) : Set := MetricSpace.mk(A, discreteDistance(A))291def metricSubspace (X S : Set) : Set :=292  MetricSpace.mk(S, subspaceMetric(MetricSpace.dist(X), S))293def productMetric (X Y : Set) : Set :=294  MetricSpace.mk(MetricSpace.carrier(X) × MetricSpace.carrier(Y),295    productDistance(MetricSpace.carrier(X), MetricSpace.dist(X),296      MetricSpace.carrier(Y), MetricSpace.dist(Y)))297298theorem realMetric.carrier299  shows MetricSpace.carrier(realMetric) = ℝ300proof301  unfold realMetric302  metric_projections303304theorem realMetric.dist305  shows MetricSpace.dist(realMetric) = realDistance306proof307  unfold realMetric308  metric_projections309310instance realMetric.space311  shows MetricSpace(realMetric)312proof313  unfold realMetric314  exact MetricSpace.of_parts with realDistance.metric315316instance realMetric.complete317  shows Complete(realMetric)318proof319  unfold realMetric320  exact Complete.of_mk with realDistance.complete321322-- The metric topology of the line is the real line.323theorem realMetric.topology324  shows metricTopology(realMetric) = realLine325proof326  unfold metricTopology327  rw [realMetric.carrier, realMetric.dist, realDistance.topology]328  unfold realLine329  rfl330331-- Convergence of a real sequence is convergence in the real metric.332theorem realMetric.converges_iff (u : Set) (L : Real)333  requires metric : MetricSpace(realMetric)334  requires sequence : u : ℕ → ℝ335  shows ConvergesTo(u, L) ↔ u ⇝ L336proof337  have realL : L ∈ MetricSpace.carrier(realMetric)338    rw realMetric.carrier339    typecheck340  have sequenceIn : u : ℕ → MetricSpace.carrier(realMetric)341    rw realMetric.carrier342    exact sequence343  have bridge := Converges.iff_parts with metric, sequenceIn344  have engine := realDistance.converges_iff at u, L345  rw [realMetric.carrier, realMetric.dist] at bridge346  constructor347  . intro converges348    exact bridge.backward with (engine.forward with converges)349  . intro converges350    exact engine.backward with (bridge.forward with converges)351352instance discreteMetric.space (A : Set)353  shows MetricSpace(discreteMetric(A))354proof355  unfold discreteMetric356  exact MetricSpace.of_parts with (discreteDistance.metric at A)357358instance discreteMetric.complete (A : Set)359  shows Complete(discreteMetric(A))360proof361  unfold discreteMetric362  exact Complete.of_mk with (discreteDistance.complete at A)363364-- The discrete metric induces the discrete topology.365theorem discreteMetric.topology (A : Set)366  shows metricTopology(discreteMetric(A)) = TopologicalSpace.mk(A, 𝒫(A))367proof368  unfold metricTopology369  unfold discreteMetric370  metric_projections371  rw discreteDistance.topology372  rfl373374instance metricSubspace.space (X S : Set)375  requires metric : MetricSpace(X)376  requires inside : S ⊆ X377  shows MetricSpace(metricSubspace(X, S))378proof379  have parts := MetricSpace.parts with metric380  unfold metricSubspace381  exact MetricSpace.of_parts with (subspaceMetric.metric with parts, inside)382383-- A closed subset of a complete space is complete.384theorem Complete.subspace (X S : Set)385  requires metric : MetricSpace(X)386  requires complete : Complete(X)387  requires closed : Closed(metricTopology(X), S)388  shows Complete(metricSubspace(X, S))389proof390  have space := MetricSpace.topological_space with metric391  have pieces := Complete.parts with complete392  have closedS := Closed.parts with space, closed393  rw [metricTopology.carrier, metricTopology.opens] at closedS394  have metricClosed : MetricClosed(X.carrier, X.dist, S)395    unfold MetricClosed396    exact closedS397  unfold metricSubspace398  exact Complete.of_mk with (IsComplete.closed_subspace with pieces,399    metricClosed)400401instance productMetric.space (X Y : Set)402  requires metricX : MetricSpace(X)403  requires metricY : MetricSpace(Y)404  shows MetricSpace(productMetric(X, Y))405proof406  have partsX := MetricSpace.parts with metricX407  have partsY := MetricSpace.parts with metricY408  unfold productMetric409  exact MetricSpace.of_parts with (productDistance.metric with partsX, partsY)410