Locally uniform convergence of metric-valued functions on compact sets

A complement to Mathlib's TendstoLocallyUniformlyOn: if functions F k with values in a pseudo-metric space converge to u locally uniformly on s, then for every compact K ⊆ s and every ε > 0, eventually dist (F k x) (u x) < ε for all x ∈ K. For real-valued functions, Real.dist_eq turns this into the bound |F k x - u x| < ε.

Conversely, if the values of F m at one point of s have norms tending to infinity, then no subsequence of F converges locally uniformly on s (TauCeti.not_tendstoLocallyUniformlyOn_comp_of_tendsto_norm_atTop), while dividing a fixed continuous function by m gives a sequence tending to 0 locally uniformly (TauCeti.tendstoLocallyUniformly_div_natCast).

theorem TendstoLocallyUniformlyOn.eventually_forall_dist_lt {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [PseudoMetricSpace β] {l : Filter ι} {F : ι → α → β} {u : α → β} {s : Set α} (hFu : TendstoLocallyUniformlyOn F u l s) {K : Set α} (hK : IsCompact K) (hKs : K ⊆ s) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (k : ι) in l, ∀ x ∈ K, dist (F k x) (u x) < ε

If functions F k converge to u locally uniformly on s, then for every compact K ⊆ s and every ε > 0, eventually dist (F k x) (u x) < ε for all x ∈ K.

theorem TauCeti.not_tendstoLocallyUniformlyOn_comp_of_tendsto_norm_atTop {α : Type u_1} [TopologicalSpace α] {s : Set α} {E : Type u_4} [SeminormedAddCommGroup E] {F : ℕ → α → E} {z : α} (hz : z ∈ s) (hF : Filter.Tendsto (fun (m : ℕ) => ‖F m z‖) Filter.atTop Filter.atTop) {φ : ℕ → ℕ} (hφ : StrictMono φ) (g : α → E) : ¬TendstoLocallyUniformlyOn (fun (m : ℕ) => F (φ m)) g Filter.atTop s

If the values of F m at a point z ∈ s have norms tending to infinity, then no subsequence of F converges locally uniformly on s, since it would converge at z.

theorem TauCeti.tendstoLocallyUniformly_div_natCast {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_4} [RCLike 𝕜] {g : α → 𝕜} (hg : Continuous g) : TendstoLocallyUniformly (fun (m : ℕ) (z : α) => g z / ↑m) (fun (x : α) => 0) Filter.atTop

For a continuous g with values in ℝ or ℂ, the maps z ↦ g z / m tend to 0 locally uniformly.