Grace/Cumulus/Metric/Continuity.g17

Open in Workbench Download source

Imports

Closed

Declarations

Source

1-- Continuity between metric spaces: the ε–δ definition, its equivalence2-- with topological continuity for the metric topologies, composition,3-- Lipschitz maps, and isometries4-- 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.Continuity10import Closed1112predicate MetricContinuousAt (f X d Y e x : Set) :=13  FunctionBetween(f, X, Y) ∧ x ∈ X ∧14  (∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧15    ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε))1617predicate IsMetricContinuous (f X d Y e : Set) :=18  FunctionBetween(f, X, Y) ∧ (∀ x ∈ X, MetricContinuousAt(f, X, d, Y, e, x))1920theorem MetricContinuousAt.function (f X d Y e x : Set)21  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)22  shows f : X → Y23proof24  exact continuous.left2526theorem MetricContinuousAt.point (f X d Y e x : Set)27  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)28  shows x ∈ X29proof30  obtain ⟨function, hx, control⟩ := continuous31  exact hx3233theorem MetricContinuousAt.control (f X d Y e x : Set, ε : Real)34  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)35  requires positive : 0 < ε36  shows ∃ δ ∈ ℝ, 0 < δ ∧ ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε)37proof38  obtain ⟨function, hx, control⟩ := continuous39  have realE : ε ∈ ℝ by typecheck40  exact control with ε, realE, positive4142theorem MetricContinuousAt.of_control (f X d Y e x : Set)43  requires function : f : X → Y44  requires hx : x ∈ X45  requires control : ∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧46    ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε)47  shows MetricContinuousAt(f, X, d, Y, e, x)48proof49  exact ⟨function, hx, control⟩5051-- Continuity at a point in terms of balls: a small ball around x is mapped52-- into any given ball around f(x).53theorem MetricContinuousAt.ball (f X d Y e x : Set, ε : Real)54  requires continuous : MetricContinuousAt(f, X, d, Y, e, x)55  requires positive : 0 < ε56  shows ∃ δ ∈ ℝ, 0 < δ ∧57    ball(X, d, x, δ) ⊆ functionPreimage(f, X, ball(Y, e, f(x), ε))58proof59  have function := MetricContinuousAt.function with continuous60  obtain ⟨δ, hδ, positiveD, maps⟩ :=61    MetricContinuousAt.control with continuous, positive62  refine ⟨δ, hδ, positiveD, ?_⟩63  intros y hy64  have hyX := ball.point with hy65  have near := ball.distance with hy66  have value := FunctionBetween.apply_closed with function, hyX67  have close := maps with y, hyX, near68  apply functionPreimage.membership.backward69  exact ⟨hyX, (ball.of_distance with value, close)⟩7071theorem MetricContinuousAt.of_ball (f X d Y e x : Set)72  requires function : f : X → Y73  requires hx : x ∈ X74  requires maps : ∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧75    ball(X, d, x, δ) ⊆ functionPreimage(f, X, ball(Y, e, f(x), ε))76  shows MetricContinuousAt(f, X, d, Y, e, x)77proof78  apply MetricContinuousAt.of_control with function, hx79  intros ε hε positive80  obtain ⟨δ, hδ, positiveD, inside⟩ := maps with ε, hε, positive81  refine ⟨δ, hδ, positiveD, ?_⟩82  intros y hy near83  have member := inside with y, (ball.of_distance with hy, near)84  have parts := functionPreimage.membership.forward with member85  exact ball.distance with parts.right8687theorem IsMetricContinuous.function (f X d Y e : Set)88  requires continuous : IsMetricContinuous(f, X, d, Y, e)89  shows f : X → Y90proof91  exact continuous.left9293theorem IsMetricContinuous.at (f X d Y e x : Set)94  requires continuous : IsMetricContinuous(f, X, d, Y, e)95  requires hx : x ∈ X96  shows MetricContinuousAt(f, X, d, Y, e, x)97proof98  exact continuous.right with x, hx99100theorem IsMetricContinuous.of_pointwise (f X d Y e : Set)101  requires function : f : X → Y102  requires pointwise : ∀ x ∈ X, MetricContinuousAt(f, X, d, Y, e, x)103  shows IsMetricContinuous(f, X, d, Y, e)104proof105  exact ⟨function, pointwise⟩106107theorem identity.metric_continuous_at (X d x : Set)108  requires hx : x ∈ X109  shows MetricContinuousAt(identity(X), X, d, X, d, x)110proof111  have function := identity.function at X112  apply MetricContinuousAt.of_control with function, hx113  intros ε hε positive114  refine ⟨ε, hε, positive, ?_⟩115  intros y hy near116  have fixedX := identity.apply with hx117  have fixedY := identity.apply with hy118  rwa [fixedX, fixedY]119120theorem identity.metric_continuous (X d : Set)121  shows IsMetricContinuous(identity(X), X, d, X, d)122proof123  apply IsMetricContinuous.of_pointwise with (identity.function at X)124  intros x hx125  exact identity.metric_continuous_at with hx126127theorem constantFunction.metric_continuous_at (X d Y e x c : Set)128  requires metric : IsMetric(Y, e)129  requires hx : x ∈ X130  requires hc : c ∈ Y131  shows MetricContinuousAt(constantFunction(X, Y, c), X, d, Y, e, x)132proof133  have function := constantFunction.function at X, Y, c with hc134  apply MetricContinuousAt.of_control with function, hx135  intros ε hε positive136  refine ⟨ε, hε, positive, ?_⟩137  intros y hy near138  have valueX := constantFunction.apply with hx, hc139  have valueY := constantFunction.apply with hy, hc140  rw [valueX, valueY]141  have self := IsMetric.self with metric, hc142  rw self143  exact positive144145theorem constantFunction.metric_continuous (X d Y e c : Set)146  requires metric : IsMetric(Y, e)147  requires hc : c ∈ Y148  shows IsMetricContinuous(constantFunction(X, Y, c), X, d, Y, e)149proof150  have function := constantFunction.function at X, Y, c with hc151  apply IsMetricContinuous.of_pointwise with function152  intros x hx153  exact constantFunction.metric_continuous_at with metric, hx, hc154155theorem MetricContinuousAt.compose (g f X d Y e Z k x : Set)156  requires first : MetricContinuousAt(f, X, d, Y, e, x)157  requires second : MetricContinuousAt(g, Y, e, Z, k, f(x))158  shows MetricContinuousAt(compose(g, f, X, Y, Z), X, d, Z, k, x)159proof160  have fFunction := MetricContinuousAt.function with first161  have gFunction := MetricContinuousAt.function with second162  have hx := MetricContinuousAt.point with first163  have composite := compose.function with fFunction, gFunction164  apply MetricContinuousAt.of_control with composite, hx165  intros ε hε positive166  obtain ⟨η, hη, positiveH, mapsG⟩ :=167    MetricContinuousAt.control with second, positive168  obtain ⟨δ, hδ, positiveD, mapsF⟩ :=169    MetricContinuousAt.control with first, positiveH170  refine ⟨δ, hδ, positiveD, ?_⟩171  intros y hy near172  have valueX := compose.apply with fFunction, gFunction, hx173  have valueY := compose.apply with fFunction, gFunction, hy174  rw [valueX, valueY]175  have middle := mapsF with y, hy, near176  have imageY := FunctionBetween.apply_closed with fFunction, hy177  exact mapsG with f(y), imageY, middle178179theorem IsMetricContinuous.compose (g f X d Y e Z k : Set)180  requires first : IsMetricContinuous(f, X, d, Y, e)181  requires second : IsMetricContinuous(g, Y, e, Z, k)182  shows IsMetricContinuous(compose(g, f, X, Y, Z), X, d, Z, k)183proof184  have fFunction := IsMetricContinuous.function with first185  have gFunction := IsMetricContinuous.function with second186  apply IsMetricContinuous.of_pointwise with (compose.function with187    fFunction, gFunction)188  intros x hx189  have image := FunctionBetween.apply_closed with fFunction, hx190  have atX := IsMetricContinuous.at with first, hx191  have atImage := IsMetricContinuous.at with second, image192  exact MetricContinuousAt.compose with atX, atImage193194-- ε–δ continuity is continuity for the metric topologies.195theorem IsMetricContinuous.continuous_map (f X d Y e : Set)196  requires metricD : IsMetric(X, d)197  requires metricE : IsMetric(Y, e)198  requires continuous : IsMetricContinuous(f, X, d, Y, e)199  shows ContinuousMap(f, X, metricTopology(X, d), Y, metricTopology(Y, e))200proof201  have function := IsMetricContinuous.function with continuous202  constructor203  . exact function204  . intros V hV205    apply metricTopology.of_open206    constructor207    . exact functionPreimage.subset at f, X, V208    . intros x hx209      have parts := functionPreimage.membership.forward with hx210      obtain ⟨ε, hε, positive, ballInside⟩ :=211        metricTopology.ball_inside with hV, parts.right212      have atX := IsMetricContinuous.at with continuous, parts.left213      obtain ⟨δ, hδ, positiveD, maps⟩ :=214        MetricContinuousAt.ball with atX, positive215      refine ⟨δ, hδ, positiveD, ?_⟩216      intros y hy217      have preimage := functionPreimage.membership.forward with (maps with218        y, hy)219      apply functionPreimage.membership.backward220      exact ⟨preimage.left, (ballInside with f(y), preimage.right)⟩221222theorem ContinuousMap.metric_continuous (f X d Y e : Set)223  requires metricD : IsMetric(X, d)224  requires metricE : IsMetric(Y, e)225  requires continuous :226    ContinuousMap(f, X, metricTopology(X, d), Y, metricTopology(Y, e))227  shows IsMetricContinuous(f, X, d, Y, e)228proof229  have function := ContinuousMap.function with continuous230  apply IsMetricContinuous.of_pointwise with function231  intros x hx232  apply MetricContinuousAt.of_ball with function, hx233  intros ε hε positive234  have image := FunctionBetween.apply_closed with function, hx235  have openBall := ball.member_topology at Y, e, f(x), ε with metricE, image236  have preimageOpen := ContinuousMap.preimage with continuous, openBall237  have center := ball.center with metricE, image, positive238  have inPreimage : x ∈ functionPreimage(f, X, ball(Y, e, f(x), ε)) :=239    functionPreimage.membership.backward with ⟨hx, center⟩240  exact metricTopology.ball_inside with preimageOpen, inPreimage241242theorem IsMetricContinuous.iff_continuous_map (f X d Y e : Set)243  requires metricD : IsMetric(X, d)244  requires metricE : IsMetric(Y, e)245  shows IsMetricContinuous(f, X, d, Y, e) ↔246    ContinuousMap(f, X, metricTopology(X, d), Y, metricTopology(Y, e))247proof248  constructor249  . intro continuous250    exact IsMetricContinuous.continuous_map with metricD, metricE, continuous251  . intro continuous252    exact ContinuousMap.metric_continuous with metricD, metricE, continuous253254-- Lipschitz maps255256predicate IsLipschitz (f X d Y e : Set) (K : Real) :=257  FunctionBetween(f, X, Y) ∧ 0 ≤ K ∧258  (∀ x ∈ X, ∀ y ∈ X, e(f(x), f(y)) ≤ realMul(K, d(x, y)))259260theorem IsLipschitz.function (f X d Y e : Set) (K : Real)261  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)262  shows f : X → Y263proof264  exact lipschitz.left265266theorem IsLipschitz.nonnegative (f X d Y e : Set) (K : Real)267  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)268  shows 0 ≤ K269proof270  obtain ⟨function, nonnegative, bound⟩ := lipschitz271  exact nonnegative272273theorem IsLipschitz.bound (f X d Y e x y : Set) (K : Real)274  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)275  requires hx : x ∈ X276  requires hy : y ∈ X277  shows e(f(x), f(y)) ≤ realMul(K, d(x, y))278proof279  obtain ⟨function, nonnegative, bound⟩ := lipschitz280  exact bound with x, hx, y, hy281282-- The modulus ε / (K + 1) works for every Lipschitz constant K ≥ 0.283theorem Lipschitz.modulus (K ε : Real)284  requires nonnegative : 0 ≤ K285  requires positive : 0 < ε286  shows 0 < ε / (K + 1) ∧ K * (ε / (K + 1)) < ε287proof288  have successorPositive : (0:R) < K + 1 by linarith289  have nonzero : K + 1 ≠ 0290    intro zero291    rw zero at successorPositive292    exact realLess.not_self with successorPositive293  have quotientReal := realDiv.real at ε, K + 1 with *294  have cancel := realDiv.mul_left at ε, K + 1 with *{2}, nonzero295  have inversePositive := realInvValue.positive with successorPositive296  have inverseReal := realInvValue.real at K + 1297  have asProduct := realDiv.eq_mul_inv at ε, K + 1 with *298  have quotientPositive : 0 < ε / (K + 1)299    rw asProduct300    exact realMulValue.positive with positive, inversePositive301  constructor302  . exact quotientPositive303  . have expand : K * (ε / (K + 1)) = ε - ε / (K + 1) by304      linear_combination cancel305    rw expand306    linarith307308theorem IsLipschitz.continuous_at (f X d Y e x : Set) (K : Real)309  requires metricD : IsMetric(X, d)310  requires metricE : IsMetric(Y, e)311  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)312  requires hx : x ∈ X313  shows MetricContinuousAt(f, X, d, Y, e, x)314proof315  have function := IsLipschitz.function with lipschitz316  have imageX := FunctionBetween.apply_closed with function, hx317  have nonnegative := IsLipschitz.nonnegative with lipschitz318  apply MetricContinuousAt.of_control with function, hx319  intros ε hε positive320  obtain ⟨positiveD, small⟩ := Lipschitz.modulus with nonnegative, positive321  have quotientReal : ε / (K + 1) ∈ ℝ by typecheck322  refine ⟨ε / (K + 1), quotientReal, positiveD, ?_⟩323  intros y hy near324  have bound := IsLipschitz.bound with lipschitz, hx, hy325  have imageY := FunctionBetween.apply_closed with function, hy326  have dxy := IsMetric.real with metricD, hx, hy327  have exy := IsMetric.real with metricE, imageX, imageY328  have le := realLess.implies_le with near329  have scaled := realLe.mul_left_of_nonnegative with le, nonnegative330  linarith331332theorem IsLipschitz.continuous (f X d Y e : Set) (K : Real)333  requires metricD : IsMetric(X, d)334  requires metricE : IsMetric(Y, e)335  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)336  shows IsMetricContinuous(f, X, d, Y, e)337proof338  apply IsMetricContinuous.of_pointwise with (IsLipschitz.function with lipschitz)339  intros x hx340  exact IsLipschitz.continuous_at with metricD, metricE, lipschitz, hx341342theorem IsLipschitz.identity (X d : Set)343  requires metric : IsMetric(X, d)344  shows IsLipschitz(identity(X), X, d, X, d, (1:R))345proof346  have one : (0:R) ≤ 1 by linarith347  unfold IsLipschitz348  constructor349  . exact identity.function at X350  . constructor351    . exact one352    . intros x hx y hy353      have fixedX := identity.apply with hx354      have fixedY := identity.apply with hy355      have dxy := IsMetric.real with metric, hx, hy356      have unit := realMulValue.one_left at d(x, y)357      rw [fixedX, fixedY, unit]358      exact realLe.reflexive359360theorem IsLipschitz.constant (X d Y e c : Set)361  requires metricD : IsMetric(X, d)362  requires metricE : IsMetric(Y, e)363  requires hc : c ∈ Y364  shows IsLipschitz(constantFunction(X, Y, c), X, d, Y, e, (0:R))365proof366  have zero : (0:R) ≤ 0 by linarith367  unfold IsLipschitz368  constructor369  . exact constantFunction.function at X, Y, c with hc370  . constructor371    . exact zero372    . intros x hx y hy373      have valueX := constantFunction.apply with hx, hc374      have valueY := constantFunction.apply with hy, hc375      have dxy := IsMetric.real with metricD, hx, hy376      have self := IsMetric.self with metricE, hc377      have annihilate := realMulValue.zero_left at d(x, y)378      rw [valueX, valueY, self, annihilate]379      exact realLe.reflexive380381theorem IsLipschitz.compose (g f X d Y e Z k : Set) (K L : Real)382  requires metricD : IsMetric(X, d)383  requires metricE : IsMetric(Y, e)384  requires metricK : IsMetric(Z, k)385  requires first : IsLipschitz(f, X, d, Y, e, K)386  requires second : IsLipschitz(g, Y, e, Z, k, L)387  shows IsLipschitz(compose(g, f, X, Y, Z), X, d, Z, k, L * K)388proof389  have fFunction := IsLipschitz.function with first390  have gFunction := IsLipschitz.function with second391  have nonnegativeK := IsLipschitz.nonnegative with first392  have nonnegativeL := IsLipschitz.nonnegative with second393  have product := realMulValue.nonnegative with nonnegativeL, nonnegativeK394  unfold IsLipschitz395  constructor396  . exact compose.function with fFunction, gFunction397  . constructor398    . exact product399    . intros x hx y hy400      have valueX := compose.apply with fFunction, gFunction, hx401      have valueY := compose.apply with fFunction, gFunction, hy402      rw [valueX, valueY]403      have imageX := FunctionBetween.apply_closed with fFunction, hx404      have imageY := FunctionBetween.apply_closed with fFunction, hy405      have inner := IsLipschitz.bound with first, hx, hy406      have outer := IsLipschitz.bound with second, imageX, imageY407      have dxy := IsMetric.real with metricD, hx, hy408      have exy := IsMetric.real with metricE, imageX, imageY409      have outerX := FunctionBetween.apply_closed with gFunction, imageX410      have outerY := FunctionBetween.apply_closed with gFunction, imageY411      have kxy := IsMetric.real with metricK, outerX, outerY412      have scaled := realLe.mul_left_of_nonnegative with inner, nonnegativeL413      have regroup : L * (K * d(x, y)) = (L * K) * d(x, y) by ring414      rw regroup at scaled415      linarith416417-- Isometries418419predicate IsIsometry (f X d Y e : Set) :=420  FunctionBetween(f, X, Y) ∧ (∀ x ∈ X, ∀ y ∈ X, e(f(x), f(y)) = d(x, y))421422theorem IsIsometry.function (f X d Y e : Set)423  requires isometry : IsIsometry(f, X, d, Y, e)424  shows f : X → Y425proof426  exact isometry.left427428theorem IsIsometry.distance (f X d Y e x y : Set)429  requires isometry : IsIsometry(f, X, d, Y, e)430  requires hx : x ∈ X431  requires hy : y ∈ X432  shows e(f(x), f(y)) = d(x, y)433proof434  exact isometry.right with x, hx, y, hy435436theorem IsIsometry.lipschitz (f X d Y e : Set)437  requires metric : IsMetric(X, d)438  requires isometry : IsIsometry(f, X, d, Y, e)439  shows IsLipschitz(f, X, d, Y, e, (1:R))440proof441  have one : (0:R) ≤ 1 by linarith442  unfold IsLipschitz443  constructor444  . exact IsIsometry.function with isometry445  . constructor446    . exact one447    . intros x hx y hy448      have preserved := IsIsometry.distance with isometry, hx, hy449      have dxy := IsMetric.real with metric, hx, hy450      have unit := realMulValue.one_left at d(x, y)451      rw [preserved, unit]452      exact realLe.reflexive453454theorem IsIsometry.continuous_at (f X d Y e x : Set)455  requires isometry : IsIsometry(f, X, d, Y, e)456  requires hx : x ∈ X457  shows MetricContinuousAt(f, X, d, Y, e, x)458proof459  have function := IsIsometry.function with isometry460  apply MetricContinuousAt.of_control with function, hx461  intros ε hε positive462  refine ⟨ε, hε, positive, ?_⟩463  intros y hy near464  have preserved := IsIsometry.distance with isometry, hx, hy465  rwa preserved466467theorem IsIsometry.continuous (f X d Y e : Set)468  requires isometry : IsIsometry(f, X, d, Y, e)469  shows IsMetricContinuous(f, X, d, Y, e)470proof471  apply IsMetricContinuous.of_pointwise with (IsIsometry.function with isometry)472  intros x hx473  exact IsIsometry.continuous_at with isometry, hx474475theorem IsIsometry.injective (f X d Y e : Set)476  requires metricD : IsMetric(X, d)477  requires metricE : IsMetric(Y, e)478  requires isometry : IsIsometry(f, X, d, Y, e)479  shows InjectiveBetween(f, X, Y)480proof481  have function := IsIsometry.function with isometry482  constructor483  . exact function484  . intros x hx y hy z hz first second485    have valueX := FunctionBetween.apply_value with function, hx, first486    have valueY := FunctionBetween.apply_value with function, hy, second487    have preserved := IsIsometry.distance with isometry, hx, hy488    have self := IsMetric.self with metricE, hz489    have zero : d(x, y) = (0:R)490      rw ← preserved491      rw [valueX, valueY]492      exact self493    exact IsMetric.eq_of_zero with metricD, hx, hy, zero494495theorem IsIsometry.compose (g f X d Y e Z k : Set)496  requires first : IsIsometry(f, X, d, Y, e)497  requires second : IsIsometry(g, Y, e, Z, k)498  shows IsIsometry(compose(g, f, X, Y, Z), X, d, Z, k)499proof500  have fFunction := IsIsometry.function with first501  have gFunction := IsIsometry.function with second502  refine ⟨(compose.function with fFunction, gFunction), ?_⟩503  intros x hx y hy504  have valueX := compose.apply with fFunction, gFunction, hx505  have valueY := compose.apply with fFunction, gFunction, hy506  rw [valueX, valueY]507  have imageX := FunctionBetween.apply_closed with fFunction, hx508  have imageY := FunctionBetween.apply_closed with fFunction, hy509  have inner := IsIsometry.distance with first, hx, hy510  have outer := IsIsometry.distance with second, imageX, imageY511  rw outer512  exact inner513514theorem identity.isometry (X d : Set)515  shows IsIsometry(identity(X), X, d, X, d)516proof517  refine ⟨(identity.function at X), ?_⟩518  intros x hx y hy519  have fixedX := identity.apply with hx520  have fixedY := identity.apply with hy521  rw [fixedX, fixedY]522  rfl523524-- An isometry maps a ball onto the ball of the image inside the image.525theorem IsIsometry.ball_image (f X d Y e x y : Set, r : Real)526  requires isometry : IsIsometry(f, X, d, Y, e)527  requires hx : x ∈ X528  requires hy : y ∈ X529  shows y ∈ ball(X, d, x, r) ↔ f(y) ∈ ball(Y, e, f(x), r)530proof531  have function := IsIsometry.function with isometry532  have preserved := IsIsometry.distance with isometry, hx, hy533  have image := FunctionBetween.apply_closed with function, hy534  constructor535  . intro member536    have near := ball.distance with member537    apply ball.of_distance with image538    rwa preserved539  . intro member540    have near := ball.distance with member541    apply ball.of_distance with hy542    rwa preserved at near543