Compact limits of approximate isometries

Maps with uniformly vanishing distance distortion and asymptotically dense images have a uniformly convergent refining ultrafilter whose limit is a surjective isometry. The approximating maps need not be continuous or measurable. Compactness and the vanishing distortion prove the uniform limit; no exact-isometry or measure-preservation conclusion is assumed.

Adapted from Freezing2/Geometry/ApproximateIsometryLimit.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

theorem BGW.MetricMeasure.isometry_of_tendsto_of_distortion {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [MetricSpace X] [MetricSpace Y] {l : Filter ι} [l.NeBot] {f : ι → X → Y} {g : X → Y} {err : ι → ℝ} (herr : Filter.Tendsto err l (nhds 0)) (hd : ∀ᶠ (i : ι) in l, ∀ (x y : X), |dist (f i x) (f i y) - dist x y| ≤ err i) (hpt : ∀ (x : X), Filter.Tendsto (fun (i : ι) => f i x) l (nhds (g x))) : Isometry g

Pointwise limits of maps with vanishing uniform distortion preserve distances.

theorem BGW.MetricMeasure.tendstoUniformly_of_tendsto_of_distortion {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [MetricSpace X] [MetricSpace Y] {l : Filter ι} [l.NeBot] {f : ι → X → Y} {g : X → Y} {err : ι → ℝ} [CompactSpace X] (herr : Filter.Tendsto err l (nhds 0)) (hd : ∀ᶠ (i : ι) in l, ∀ (x y : X), |dist (f i x) (f i y) - dist x y| ≤ err i) (hpt : ∀ (x : X), Filter.Tendsto (fun (i : ι) => f i x) l (nhds (g x))) : TendstoUniformly f g l

On a compact domain the same vanishing distortion upgrades pointwise convergence to uniform convergence, even for discontinuous approximants.

theorem BGW.MetricMeasure.surjective_of_tendstoUniformly_of_dense {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [MetricSpace X] [MetricSpace Y] {l : Filter ι} [l.NeBot] {f : ι → X → Y} {g : X → Y} {err : ι → ℝ} [CompactSpace X] (hg : Isometry g) (herr : Filter.Tendsto err l (nhds 0)) (hdense : ∀ᶠ (i : ι) in l, ∀ (y : Y), ∃ (x : X), dist y (f i x) ≤ err i) (huni : TendstoUniformly f g l) : Function.Surjective g

A uniform isometric limit of asymptotically dense maps is surjective.

theorem BGW.MetricMeasure.exists_isometryEquiv_uniform_limit_of_distortion {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [MetricSpace X] [MetricSpace Y] {l : Filter ι} [l.NeBot] {f : ι → X → Y} {err : ι → ℝ} [CompactSpace X] [CompactSpace Y] (herr : Filter.Tendsto err l (nhds 0)) (hd : ∀ᶠ (i : ι) in l, ∀ (x y : X), |dist (f i x) (f i y) - dist x y| ≤ err i) (hdense : ∀ᶠ (i : ι) in l, ∀ (y : Y), ∃ (x : X), dist y (f i x) ≤ err i) : ∃ (U : Ultrafilter ι), ↑U ≤ l ∧ ∃ (e : X ≃ᵢ Y), TendstoUniformly f ⇑e ↑U

Compactness supplies a refining ultrafilter and a genuine surjective isometry as its uniform limit. No continuity of the approximants is required.