Grace/Cumulus/Metric/Maps.g17

Open in Workbench Download source

Imports

Limits

Declarations

Source

1-- Lipschitz maps and isometries, continued: restrictions to subspaces,2-- images of balls, inverses of bijective isometries as homeomorphisms,3-- and the distance to a fixed point as a 1-Lipschitz real function4-- 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.Maps10import Limits1112theorem IsLipschitz.of_le (f X d Y e : Set) (K L : Real)13  requires metricD : IsMetric(X, d)14  requires metricE : IsMetric(Y, e)15  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)16  requires le : K ≤ L17  shows IsLipschitz(f, X, d, Y, e, L)18proof19  have function := IsLipschitz.function with lipschitz20  have nonnegativeK := IsLipschitz.nonnegative with lipschitz21  have nonnegativeL : 0 ≤ L by linarith22  unfold IsLipschitz23  constructor24  . exact function25  . constructor26    . exact nonnegativeL27    . intros x hx y hy28      have bound := IsLipschitz.bound with lipschitz, hx, hy29      have dxy := IsMetric.real with metricD, hx, hy30      have imageX := FunctionBetween.apply_closed with function, hx31      have imageY := FunctionBetween.apply_closed with function, hy32      have exy := IsMetric.real with metricE, imageX, imageY33      have nonnegative := IsMetric.nonnegative with metricD, hx, hy34      have scaled := realLe.mul_right_of_nonnegative with le, nonnegative35      linarith3637-- A Lipschitz map with constant zero is constant.38theorem IsLipschitz.constant_of_zero (f X d Y e x y : Set)39  requires metricD : IsMetric(X, d)40  requires metricE : IsMetric(Y, e)41  requires lipschitz : IsLipschitz(f, X, d, Y, e, (0:R))42  requires hx : x ∈ X43  requires hy : y ∈ X44  shows f(x) = f(y)45proof46  have function := IsLipschitz.function with lipschitz47  have bound := IsLipschitz.bound with lipschitz, hx, hy48  have dxy := IsMetric.real with metricD, hx, hy49  have imageX := FunctionBetween.apply_closed with function, hx50  have imageY := FunctionBetween.apply_closed with function, hy51  have exy := IsMetric.real with metricE, imageX, imageY52  have nonnegative := IsMetric.nonnegative with metricE, imageX, imageY53  have annihilate := realMulValue.zero_left at d(x, y)54  rw annihilate at bound55  have zero : e(f(x), f(y)) = (0:R) by linarith56  exact IsMetric.eq_of_zero with metricE, imageX, imageY, zero5758theorem IsLipschitz.restrict (f X d Y e S : Set) (K : Real)59  requires metric : IsMetric(X, d)60  requires inside : S ⊆ X61  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)62  shows IsLipschitz(restrict(f, S), S, subspaceMetric(d, S), Y, e, K)63proof64  have function := IsLipschitz.function with lipschitz65  have nonnegative := IsLipschitz.nonnegative with lipschitz66  unfold IsLipschitz67  constructor68  . exact restrict.domain_function with function, inside69  . constructor70    . exact nonnegative71    . intros x hx y hy72      have valueX := restrict.domain_apply with function, inside, hx73      have valueY := restrict.domain_apply with function, inside, hy74      have distance := subspaceMetric.apply with metric, inside, hx, hy75      rw [valueX, valueY, distance]76      exact IsLipschitz.bound with lipschitz, (inside with x, hx), (inside with77        y, hy)7879theorem IsIsometry.restrict (f X d Y e S : Set)80  requires metric : IsMetric(X, d)81  requires inside : S ⊆ X82  requires isometry : IsIsometry(f, X, d, Y, e)83  shows IsIsometry(restrict(f, S), S, subspaceMetric(d, S), Y, e)84proof85  have function := IsIsometry.function with isometry86  constructor87  . exact restrict.domain_function with function, inside88  . intros x hx y hy89    have valueX := restrict.domain_apply with function, inside, hx90    have valueY := restrict.domain_apply with function, inside, hy91    have distance := subspaceMetric.apply with metric, inside, hx, hy92    rw [valueX, valueY, distance]93    exact IsIsometry.distance with isometry, (inside with x, hx), (inside with94      y, hy)9596theorem IsUniformlyContinuous.restrict (f X d Y e S : Set)97  requires metric : IsMetric(X, d)98  requires inside : S ⊆ X99  requires uniform : IsUniformlyContinuous(f, X, d, Y, e)100  shows IsUniformlyContinuous(restrict(f, S), S, subspaceMetric(d, S), Y, e)101proof102  have function := IsUniformlyContinuous.function with uniform103  apply IsUniformlyContinuous.of_control with (restrict.domain_function with104    function, inside)105  intros ε hε positive106  obtain ⟨δ, hδ, positiveD, maps⟩ :=107    IsUniformlyContinuous.control with uniform, positive108  refine ⟨δ, hδ, positiveD, ?_⟩109  intros x hx y hy near110  have valueX := restrict.domain_apply with function, inside, hx111  have valueY := restrict.domain_apply with function, inside, hy112  have distance := subspaceMetric.apply with metric, inside, hx, hy113  rw distance at near114  rw [valueX, valueY]115  exact maps with x, (inside with x, hx), y, (inside with y, hy), near116117theorem MetricContinuousAt.restrict (f X d Y e S x : Set)118  requires metric : IsMetric(X, d)119  requires inside : S ⊆ X120  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)121  requires hx : x ∈ S122  shows MetricContinuousAt(restrict(f, S), S, subspaceMetric(d, S), Y, e, x)123proof124  have function := MetricContinuousAt.function with continuous125  have restricted := restrict.domain_function with function, inside126  apply MetricContinuousAt.of_control with restricted, hx127  intros ε hε positive128  obtain ⟨δ, hδ, positiveD, maps⟩ :=129    MetricContinuousAt.control with continuous, positive130  refine ⟨δ, hδ, positiveD, ?_⟩131  intros y hy near132  have valueX := restrict.domain_apply with function, inside, hx133  have valueY := restrict.domain_apply with function, inside, hy134  have distance := subspaceMetric.apply with metric, inside, hx, hy135  rw distance at near136  rw [valueX, valueY]137  exact maps with y, (inside with y, hy), near138139theorem inclusionMap.lipschitz (X d S : Set)140  requires metric : IsMetric(X, d)141  requires inside : S ⊆ X142  shows IsLipschitz(inclusionMap(S, X), S, subspaceMetric(d, S), X, d, (1:R))143proof144  have subspace := subspaceMetric.metric with metric, inside145  exact IsIsometry.lipschitz with subspace, (inclusionMap.isometry with146    metric, inside)147148theorem inclusionMap.uniformly_continuous (X d S : Set)149  requires metric : IsMetric(X, d)150  requires inside : S ⊆ X151  shows IsUniformlyContinuous(inclusionMap(S, X), S, subspaceMetric(d, S), X, d)152proof153  exact IsIsometry.uniformly_continuous with (inclusionMap.isometry with154    metric, inside)155156-- Images of balls under Lipschitz maps and isometries.157theorem IsLipschitz.image_ball (f X d Y e x : Set) (K r : Real)158  requires metricD : IsMetric(X, d)159  requires metricE : IsMetric(Y, e)160  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)161  requires positive : 0 < K162  requires hx : x ∈ X163  shows functionImage(f, ball(X, d, x, r), Y) ⊆ ball(Y, e, f(x), K * r)164proof165  have function := IsLipschitz.function with lipschitz166  intros v hv167  obtain ⟨hvY, y, hy, shape⟩ := functionImage.membership.forward with hv168  rw shape169  have hyX := ball.point with hy170  have near := ball.distance with hy171  have bound := IsLipschitz.bound with lipschitz, hx, hyX172  have dxy := IsMetric.real with metricD, hx, hyX173  have imageX := FunctionBetween.apply_closed with function, hx174  have imageY := FunctionBetween.apply_closed with function, hyX175  have exy := IsMetric.real with metricE, imageX, imageY176  have scaled := realLess.mul_left_of_positive with near, positive177  apply ball.of_distance with imageY178  linarith179180theorem IsLipschitz.image_closedBall (f X d Y e x : Set) (K r : Real)181  requires metricD : IsMetric(X, d)182  requires metricE : IsMetric(Y, e)183  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)184  requires hx : x ∈ X185  shows186    functionImage(f, closedBall(X, d, x, r), Y) ⊆ closedBall(Y, e, f(x), K * r)187proof188  have function := IsLipschitz.function with lipschitz189  have nonnegative := IsLipschitz.nonnegative with lipschitz190  intros v hv191  obtain ⟨hvY, y, hy, shape⟩ := functionImage.membership.forward with hv192  rw shape193  have hyX := closedBall.point with hy194  have near := closedBall.distance with hy195  have bound := IsLipschitz.bound with lipschitz, hx, hyX196  have dxy := IsMetric.real with metricD, hx, hyX197  have imageX := FunctionBetween.apply_closed with function, hx198  have imageY := FunctionBetween.apply_closed with function, hyX199  have exy := IsMetric.real with metricE, imageX, imageY200  have scaled := realLe.mul_left_of_nonnegative with near, nonnegative201  apply closedBall.of_distance with imageY202  linarith203204theorem IsIsometry.image_ball_subset (f X d Y e x : Set, r : Real)205  requires isometry : IsIsometry(f, X, d, Y, e)206  requires hx : x ∈ X207  shows functionImage(f, ball(X, d, x, r), Y) ⊆ ball(Y, e, f(x), r)208proof209  intros v hv210  obtain ⟨hvY, y, hy, shape⟩ := functionImage.membership.forward with hv211  rw shape212  have hyX := ball.point with hy213  have characterization := IsIsometry.ball_image at f, X, d, Y, e, x, y, r with214    isometry, hx, hyX215  exact characterization.forward with hy216217theorem IsIsometry.closedBall_image (f X d Y e x y : Set, r : Real)218  requires isometry : IsIsometry(f, X, d, Y, e)219  requires hx : x ∈ X220  requires hy : y ∈ X221  shows y ∈ closedBall(X, d, x, r) ↔ f(y) ∈ closedBall(Y, e, f(x), r)222proof223  have function := IsIsometry.function with isometry224  have preserved := IsIsometry.distance with isometry, hx, hy225  have image := FunctionBetween.apply_closed with function, hy226  constructor227  . intro member228    have near := closedBall.distance with member229    apply closedBall.of_distance with image230    rwa preserved231  . intro member232    have near := closedBall.distance with member233    apply closedBall.of_distance with hy234    rwa preserved at near235236theorem IsIsometry.sphere_image (f X d Y e x y : Set, r : Real)237  requires isometry : IsIsometry(f, X, d, Y, e)238  requires hx : x ∈ X239  requires hy : y ∈ X240  shows y ∈ sphere(X, d, x, r) ↔ f(y) ∈ sphere(Y, e, f(x), r)241proof242  have function := IsIsometry.function with isometry243  have preserved := IsIsometry.distance with isometry, hx, hy244  have image := FunctionBetween.apply_closed with function, hy245  constructor246  . intro member247    obtain ⟨hyX, equal⟩ := sphere.membership.forward with member248    apply sphere.membership.backward249    refine ⟨image, ?_⟩250    rwa preserved251  . intro member252    obtain ⟨imageY, equal⟩ := sphere.membership.forward with member253    apply sphere.membership.backward254    refine ⟨hy, ?_⟩255    rwa preserved at equal256257theorem IsIsometry.image_bounded (f X d Y e S : Set)258  requires metricD : IsMetric(X, d)259  requires metricE : IsMetric(Y, e)260  requires isometry : IsIsometry(f, X, d, Y, e)261  requires bounded : IsBounded(X, d, S)262  shows IsBounded(Y, e, functionImage(f, S, Y))263proof264  have lipschitz := IsIsometry.lipschitz with metricD, isometry265  exact IsLipschitz.image_bounded with metricD, metricE, lipschitz, bounded266267theorem IsLipschitz.converges (f X d Y e u x : Set) (K : Real)268  requires metricD : IsMetric(X, d)269  requires metricE : IsMetric(Y, e)270  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)271  requires converges : ConvergesIn(X, d, u, x)272  shows ConvergesIn(Y, e, compose(f, u, ℕ, X, Y), f(x))273proof274  have continuous := IsLipschitz.continuous with metricD, metricE, lipschitz275  exact ConvergesIn.map_continuous with continuous, converges276277-- The inverse of a bijective isometry is an isometry, so a bijective278-- isometry is a homeomorphism of the metric topologies.279theorem IsIsometry.inverse (f X d Y e : Set)280  requires isometry : IsIsometry(f, X, d, Y, e)281  requires bijective : BijectiveBetween(f, X, Y)282  shows IsIsometry(converse(f, X, Y), Y, e, X, d)283proof284  have inverse := converse.function_of_bijective with bijective285  constructor286  . exact inverse287  . intros v hv w hw288    have preimageV := FunctionBetween.apply_closed with inverse, hv289    have preimageW := FunctionBetween.apply_closed with inverse, hw290    have preserved := IsIsometry.distance with isometry, preimageV, preimageW291    have backV := Bijective.apply_inverse with bijective, hv292    have backW := Bijective.apply_inverse with bijective, hw293    rw [backV, backW] at preserved294    symm at preserved295    exact preserved296297theorem IsIsometry.inverse_continuous (f X d Y e : Set)298  requires isometry : IsIsometry(f, X, d, Y, e)299  requires bijective : BijectiveBetween(f, X, Y)300  shows IsMetricContinuous(converse(f, X, Y), Y, e, X, d)301proof302  exact IsIsometry.continuous with (IsIsometry.inverse with isometry, bijective)303304theorem IsIsometry.inverse_uniformly_continuous (f X d Y e : Set)305  requires isometry : IsIsometry(f, X, d, Y, e)306  requires bijective : BijectiveBetween(f, X, Y)307  shows IsUniformlyContinuous(converse(f, X, Y), Y, e, X, d)308proof309  exact IsIsometry.uniformly_continuous with (IsIsometry.inverse with310    isometry, bijective)311312theorem IsIsometry.homeomorphism (f X d Y e : Set)313  requires metricD : IsMetric(X, d)314  requires metricE : IsMetric(Y, e)315  requires isometry : IsIsometry(f, X, d, Y, e)316  requires bijective : BijectiveBetween(f, X, Y)317  shows IsHomeomorphism(f, X, metricTopology(X, d), Y, metricTopology(Y, e))318proof319  have forward := IsIsometry.continuous with isometry320  have backward := IsIsometry.inverse_continuous with isometry, bijective321  refine ⟨bijective, ?_, ?_⟩322  . exact IsMetricContinuous.continuous_map with metricD, metricE, forward323  . exact IsMetricContinuous.continuous_map with metricE, metricD, backward324325-- The distance to a fixed point, as a real-valued function on the space.326defgraph distanceTo (X d y : Set) (x ∈ X) : ℝ := d(x, y)327requires metric : IsMetric(X, d)328requires hy : y ∈ X329proof330  exact IsMetric.real with metric, member, hy331332theorem distanceTo.nonnegative (X d y x : Set)333  requires metric : IsMetric(X, d)334  requires hy : y ∈ X335  requires hx : x ∈ X336  shows (0:R) ≤ distanceTo(X, d, y)(x)337proof338  have value := distanceTo.value at X, d, y, x with metric, hy, hx339  rw value340  exact IsMetric.nonnegative with metric, hx, hy341342theorem distanceTo.zero_iff (X d y x : Set)343  requires metric : IsMetric(X, d)344  requires hy : y ∈ X345  requires hx : x ∈ X346  shows distanceTo(X, d, y)(x) = (0:R) ↔ x = y347proof348  have value := distanceTo.value at X, d, y, x with metric, hy, hx349  rw value350  exact IsMetric.eq_zero_iff with metric, hx, hy351352theorem distanceTo.lipschitz (X d y : Set)353  requires metric : IsMetric(X, d)354  requires hy : y ∈ X355  shows IsLipschitz(distanceTo(X, d, y), X, d, ℝ, realDistance, (1:R))356proof357  have one : (0:R) ≤ 1 by linarith358  unfold IsLipschitz359  constructor360  . exact distanceTo.function with metric, hy361  . constructor362    . exact one363    . intros x hx z hz364      have valueX := distanceTo.value at X, d, y, x with metric, hy, hx365      have valueZ := distanceTo.value at X, d, y, z with metric, hy, hz366      rw [valueX, valueZ]367      have dxy := IsMetric.real with metric, hx, hy368      have dzy := IsMetric.real with metric, hz, hy369      have dxz := IsMetric.real with metric, hx, hz370      have realValue := realDistance.apply at d(x, y), d(z, y) with *371      rw realValue372      unfold dist373      have reverse := IsMetric.abs_sub_le with metric, hx, hz, hy374      have unit := realMulValue.one_left at d(x, z)375      rw unit376      exact reverse377378theorem distanceTo.uniformly_continuous (X d y : Set)379  requires metric : IsMetric(X, d)380  requires hy : y ∈ X381  shows IsUniformlyContinuous(distanceTo(X, d, y), X, d, ℝ, realDistance)382proof383  have lipschitz := distanceTo.lipschitz with metric, hy384  exact IsLipschitz.uniformly_continuous with385    metric, realDistance.metric, lipschitz386387theorem distanceTo.continuous (X d y : Set)388  requires metric : IsMetric(X, d)389  requires hy : y ∈ X390  shows IsMetricContinuous(distanceTo(X, d, y), X, d, ℝ, realDistance)391proof392  have uniform := distanceTo.uniformly_continuous with metric, hy393  exact IsUniformlyContinuous.continuous with uniform394395theorem distanceTo.converges (X d y u x : Set)396  requires metric : IsMetric(X, d)397  requires hy : y ∈ X398  requires converges : ConvergesIn(X, d, u, x)399  shows ConvergesIn(ℝ, realDistance, compose(distanceTo(X, d, y), u, ℕ, X, ℝ),400    distanceTo(X, d, y)(x))401proof402  have continuous := distanceTo.continuous with metric, hy403  exact ConvergesIn.map_continuous with continuous, converges404405theorem distanceTo.ball_preimage (X d y : Set, r : Real)406  requires metric : IsMetric(X, d)407  requires hy : y ∈ X408  shows409    ball(X, d, y, r) = functionPreimage(distanceTo(X, d, y), X, openBall(0, r))410proof411  ext x412  constructor413  . intro hx414    have hxX := ball.point with hx415    have near := ball.distance with hx416    have value := distanceTo.value at X, d, y, x with metric, hy, hxX417    have symmetric := IsMetric.symmetric with metric, hy, hxX418    have dxy := IsMetric.real with metric, hxX, hy419    have nonnegative := IsMetric.nonnegative with metric, hxX, hy420    apply functionPreimage.membership.backward421    refine ⟨hxX, ?_⟩422    rw value423    apply openBall.membership.backward424    refine ⟨dxy, ?_⟩425    unfold dist426    have zero := realSubValue.zero_right at d(x, y)427    have unfolded := abs.of_nonnegative with nonnegative428    rw [zero, unfolded]429    rwa symmetric at near430  . intro hx431    obtain ⟨hxX, inBall⟩ := functionPreimage.membership.forward with hx432    have value := distanceTo.value at X, d, y, x with metric, hy, hxX433    rw value at inBall434    have symmetric := IsMetric.symmetric with metric, hy, hxX435    have dxy := IsMetric.real with metric, hxX, hy436    have nonnegative := IsMetric.nonnegative with metric, hxX, hy437    obtain ⟨valueReal, near⟩ := openBall.membership.forward with inBall438    unfold dist at near439    have zero := realSubValue.zero_right at d(x, y)440    have unfolded := abs.of_nonnegative with nonnegative441    rw [zero, unfolded] at near442    apply ball.of_distance with hxX443    rwa symmetric444