Grace/Cumulus/Metric/Uniform.g17

Open in Workbench Download source

Imports

Bounded

Declarations

• IsUniformlyContinuous predicate
• IsUniformlyContinuous.function theorem derivation
• IsUniformlyContinuous.control theorem derivation
• IsUniformlyContinuous.of_control theorem derivation
• IsUniformlyContinuous.continuous_at theorem derivation
• IsUniformlyContinuous.continuous theorem derivation
• IsLipschitz.uniformly_continuous theorem derivation
• IsIsometry.uniformly_continuous theorem derivation
• identity.uniformly_continuous theorem derivation
• constantFunction.uniformly_continuous theorem derivation
• IsUniformlyContinuous.compose theorem derivation
• IsUniformlyContinuous.cauchy theorem derivation
• IsUniformlyContinuous.of_isometry_compose theorem derivation

Source

1-- Uniform continuity between metric spaces: Lipschitz maps and isometries2-- are uniformly continuous, uniformly continuous maps are continuous,3-- compose, and preserve Cauchy sequences4-- 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.Uniform10import Bounded1112predicate IsUniformlyContinuous (f X d Y e : Set) :=13  FunctionBetween(f, X, Y) ∧14  (∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧15    ∀ x ∈ X, ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε))1617theorem IsUniformlyContinuous.function (f X d Y e : Set)18  requires uniform : IsUniformlyContinuous(f, X, d, Y, e)19  shows f : X → Y20proof21  exact uniform.left2223theorem IsUniformlyContinuous.control (f X d Y e : Set, ε : Real)24  requires uniform : IsUniformlyContinuous(f, X, d, Y, e)25  requires positive : 0 < ε26  shows ∃ δ ∈ ℝ, 0 < δ ∧ ∀ x ∈ X, ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε)27proof28  obtain ⟨function, control⟩ := uniform29  have realE : ε ∈ ℝ by typecheck30  exact control with ε, realE, positive3132theorem IsUniformlyContinuous.of_control (f X d Y e : Set)33  requires function : f : X → Y34  requires control : ∀ ε ∈ ℝ, 0 < ε → ∃ δ ∈ ℝ, 0 < δ ∧35    ∀ x ∈ X, ∀ y ∈ X, (d(x, y) < δ → e(f(x), f(y)) < ε)36  shows IsUniformlyContinuous(f, X, d, Y, e)37proof38  exact ⟨function, control⟩3940theorem IsUniformlyContinuous.continuous_at (f X d Y e x : Set)41  requires uniform : IsUniformlyContinuous(f, X, d, Y, e)42  requires hx : x ∈ X43  shows MetricContinuousAt(f, X, d, Y, e, x)44proof45  have function := IsUniformlyContinuous.function with uniform46  apply MetricContinuousAt.of_control with function, hx47  intros ε hε positive48  obtain ⟨δ, hδ, positiveD, maps⟩ :=49    IsUniformlyContinuous.control with uniform, positive50  refine ⟨δ, hδ, positiveD, ?_⟩51  intros y hy near52  exact maps with x, hx, y, hy, near5354theorem IsUniformlyContinuous.continuous (f X d Y e : Set)55  requires uniform : IsUniformlyContinuous(f, X, d, Y, e)56  shows IsMetricContinuous(f, X, d, Y, e)57proof58  apply IsMetricContinuous.of_pointwise with (IsUniformlyContinuous.function with59    uniform)60  intros x hx61  exact IsUniformlyContinuous.continuous_at with uniform, hx6263theorem IsLipschitz.uniformly_continuous (f X d Y e : Set) (K : Real)64  requires metricD : IsMetric(X, d)65  requires metricE : IsMetric(Y, e)66  requires lipschitz : IsLipschitz(f, X, d, Y, e, K)67  shows IsUniformlyContinuous(f, X, d, Y, e)68proof69  have function := IsLipschitz.function with lipschitz70  have nonnegative := IsLipschitz.nonnegative with lipschitz71  apply IsUniformlyContinuous.of_control with function72  intros ε hε positive73  obtain ⟨positiveD, small⟩ := Lipschitz.modulus with nonnegative, positive74  have quotientReal : ε / (K + 1) ∈ ℝ by typecheck75  refine ⟨ε / (K + 1), quotientReal, positiveD, ?_⟩76  intros x hx y hy near77  have bound := IsLipschitz.bound with lipschitz, hx, hy78  have imageX := FunctionBetween.apply_closed with function, hx79  have imageY := FunctionBetween.apply_closed with function, hy80  have dxy := IsMetric.real with metricD, hx, hy81  have exy := IsMetric.real with metricE, imageX, imageY82  have le := realLess.implies_le with near83  have scaled := realLe.mul_left_of_nonnegative with le, nonnegative84  linarith8586theorem IsIsometry.uniformly_continuous (f X d Y e : Set)87  requires isometry : IsIsometry(f, X, d, Y, e)88  shows IsUniformlyContinuous(f, X, d, Y, e)89proof90  have function := IsIsometry.function with isometry91  apply IsUniformlyContinuous.of_control with function92  intros ε hε positive93  refine ⟨ε, hε, positive, ?_⟩94  intros x hx y hy near95  have preserved := IsIsometry.distance with isometry, hx, hy96  rwa preserved9798theorem identity.uniformly_continuous (X d : Set)99  shows IsUniformlyContinuous(identity(X), X, d, X, d)100proof101  exact IsIsometry.uniformly_continuous with (identity.isometry at X, d)102103theorem constantFunction.uniformly_continuous (X d Y e c : Set)104  requires metric : IsMetric(Y, e)105  requires hc : c ∈ Y106  shows IsUniformlyContinuous(constantFunction(X, Y, c), X, d, Y, e)107proof108  have function := constantFunction.function at X, Y, c with hc109  apply IsUniformlyContinuous.of_control with function110  intros ε hε positive111  refine ⟨ε, hε, positive, ?_⟩112  intros x hx y hy near113  have valueX := constantFunction.apply with hx, hc114  have valueY := constantFunction.apply with hy, hc115  rw [valueX, valueY]116  have self := IsMetric.self with metric, hc117  rw self118  exact positive119120theorem IsUniformlyContinuous.compose (g f X d Y e Z k : Set)121  requires first : IsUniformlyContinuous(f, X, d, Y, e)122  requires second : IsUniformlyContinuous(g, Y, e, Z, k)123  shows IsUniformlyContinuous(compose(g, f, X, Y, Z), X, d, Z, k)124proof125  have fFunction := IsUniformlyContinuous.function with first126  have gFunction := IsUniformlyContinuous.function with second127  apply IsUniformlyContinuous.of_control with (compose.function with128    fFunction, gFunction)129  intros ε hε positive130  obtain ⟨η, hη, positiveH, mapsG⟩ :=131    IsUniformlyContinuous.control with second, positive132  obtain ⟨δ, hδ, positiveD, mapsF⟩ :=133    IsUniformlyContinuous.control with first, positiveH134  refine ⟨δ, hδ, positiveD, ?_⟩135  intros x hx y hy near136  have valueX := compose.apply with fFunction, gFunction, hx137  have valueY := compose.apply with fFunction, gFunction, hy138  rw [valueX, valueY]139  have imageX := FunctionBetween.apply_closed with fFunction, hx140  have imageY := FunctionBetween.apply_closed with fFunction, hy141  have middle := mapsF with x, hx, y, hy, near142  exact mapsG with f(x), imageX, f(y), imageY, middle143144-- Uniformly continuous maps send Cauchy sequences to Cauchy sequences.145theorem IsUniformlyContinuous.cauchy (f X d Y e u : Set)146  requires uniform : IsUniformlyContinuous(f, X, d, Y, e)147  requires cauchy : IsCauchy(X, d, u)148  shows IsCauchy(Y, e, compose(f, u, ℕ, X, Y))149proof150  have function := IsUniformlyContinuous.function with uniform151  have sequence := IsCauchy.sequence with cauchy152  have uFunction := SequenceIn.function with sequence153  have composite := SequenceIn.compose with sequence, function154  apply IsCauchy.of_eventually with composite155  intros ε hε positive156  obtain ⟨δ, hδ, positiveD, maps⟩ :=157    IsUniformlyContinuous.control with uniform, positive158  obtain ⟨N, hN, close⟩ := IsCauchy.eventually with cauchy, positiveD159  refine ⟨N, hN, ?_⟩160  intros m hm n hn leM leN161  have termM := SequenceIn.term_of_member with sequence, hm162  have termN := SequenceIn.term_of_member with sequence, hn163  have valueM := compose.apply with uFunction, function, hm164  have valueN := compose.apply with uFunction, function, hn165  rw [valueM, valueN]166  exact maps with u(m), termM, u(n), termN, (close with m, hm, n, hn, leM, leN)167168theorem IsUniformlyContinuous.of_isometry_compose (g f X d Y e Z k : Set)169  requires isometry : IsIsometry(f, X, d, Y, e)170  requires uniform : IsUniformlyContinuous(g, Y, e, Z, k)171  shows IsUniformlyContinuous(compose(g, f, X, Y, Z), X, d, Z, k)172proof173  have first := IsIsometry.uniformly_continuous with isometry174  exact IsUniformlyContinuous.compose with first, uniform175