Bounded perturbations of proper maps

A continuous map at uniformly bounded distance from a proper map into a proper metric space is proper. For example, a uniformly small smooth perturbation of a proper real-valued exhaustion function remains proper. The source needs no metric or separation assumptions.

The proof uses Mathlib's compactness of closed thickenings in proper metric spaces: the inverse image of a compact set under the perturbed map is a closed subset of the original map's inverse image of a compact thickening.

In a proper normed group the squared distance v ↦ ‖v - a‖ ^ 2 from a point tends to infinity along the cocompact filter, so it is proper, and so is its composition with any closed embedding. These are the squared-distance exhaustions of closed subsets of Euclidean space used in Morse theory. Conversely, along a continuous map the squared distance is proper only if the map is proper, so along the inclusion of a subset only if the subset is closed (TauCeti.isProperMap_norm_sq_sub_comp_iff, TauCeti.isProperMap_norm_sq_sub_subtypeVal_iff). For example, in a normed group punctured at a non-isolated point y, the bounded sublevel {v | ‖v - a‖² ≤ r} accumulates at the puncture and is not compact when ‖y - a‖² < r (TauCeti.not_isCompact_compl_singleton_inter_preimage_Iic), so the squared distance is not proper (TauCeti.not_isProperMap_norm_sq_sub_compl_singleton).

theorem IsProperMap.of_dist_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MetricSpace Y] [ProperSpace Y] {f g : X → Y} (hf : IsProperMap f) (hg : Continuous g) {C : ℝ} (hfg : ∀ (x : X), dist (f x) (g x) ≤ C) : IsProperMap g

A continuous map at uniformly bounded distance from a proper map into a proper metric space is proper. The bound need not be positive; this includes maps from an empty space.

theorem TauCeti.isProperMap_norm_sq_sub {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] (a : E) : IsProperMap fun (v : E) => ‖v - a‖ ^ 2

In a proper normed group, the squared distance from a point is a proper map.

theorem TauCeti.isProperMap_norm_sq_sub_comp {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [ProperSpace E] {i : X → E} (hi : Topology.IsClosedEmbedding i) (a : E) : IsProperMap fun (x : X) => ‖i x - a‖ ^ 2

The squared distance from a point along a closed embedding into a proper normed group is a proper map.

theorem TauCeti.isProperMap_norm_sq_sub_comp_iff {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [ProperSpace E] {i : X → E} (hi : Continuous i) (a : E) : (IsProperMap fun (x : X) => ‖i x - a‖ ^ 2) ↔ IsProperMap i

Along a continuous map into a proper normed group, the squared distance from a point is a proper map exactly when the map itself is proper.

theorem TauCeti.isProperMap_norm_sq_sub_subtypeVal_iff {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] {S : Set E} (a : E) : (IsProperMap fun (x : ↑S) => ‖↑x - a‖ ^ 2) ↔ IsClosed S

The squared distance from a point, restricted to a subset of a proper normed group, is a proper map exactly when the subset is closed.

theorem TauCeti.not_isCompact_compl_singleton_inter_preimage_Iic {F : Type u_1} [NormedAddCommGroup F] {y a : F} [(nhdsWithin y {y}ᶜ).NeBot] {r : ℝ} (hr : ‖y - a‖ ^ 2 < r) : ¬IsCompact ({y}ᶜ ∩ (fun (v : F) => ‖v - a‖ ^ 2) ⁻¹' Set.Iic r)

In a normed group punctured at a non-isolated point y, the bounded sublevel {ρ_a ≤ r} of the squared distance from a is not compact when ‖y - a‖² < r: it accumulates at the puncture.

theorem TauCeti.not_isProperMap_norm_sq_sub_compl_singleton {F : Type u_1} [NormedAddCommGroup F] (y a : F) [(nhdsWithin y {y}ᶜ).NeBot] : ¬IsProperMap fun (x : ↑{y}ᶜ) => ‖↑x - a‖ ^ 2

On a normed group punctured at a non-isolated point y, the squared distance from any point is not a proper map.