Commit 2025-06-19 08:56 15948de6

feat: define a metric structure on α →ᵤ β (#25827) When β is a (pseudo, extended) metric space, the space of function α →ᵤ β equipped with the topology of uniform convergence is naturally a (pseudo, extended) metric space with distance given by edist f g := ⨆ x, edist (f x) (g x) (and this induces the pre-existing uniformity on α →ᵤ β). Likewise for α →ᵤ[𝔖] β with 𝔖 finite, ⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x) is a natural metric which induces the existing uniformity. In certain situations, α →ᵤ[𝔖] β is metrizable even if 𝔖 is not finite, but in these cases, the above is not a suitable distance function. As an example, if β is a σ-compact metric space, then UniformOnFun.isCountablyGenerated_uniformity guarantees that α →ᵤ[{K | IsCompact K}] β is metrizable, but since the union of the compact sets is the entire space, the metric above would generate the topology of uniform convergence (everywhere, not just on compact sets). In this PR, we provide these instances, and derive several consequences. For example, we derive the natural sufficient condition for uniform equicontinuity in terms of the individual functions being Lipschitz with the same constant:

lemma LipschitzWith.uniformEquicontinuous (f : α → γ → β) (K : ℝ≥0)
    (h : ∀ c, LipschitzWith K (f c)) : UniformEquicontinuous f := 
  sorry

In addition, we prove that the natural maps from BoundedContinuousFunction and ContinuousMap (when the domain is compact) are isometries. This is all motivated by the desire to state joint continuity results for the continuous functional calculus (cfc) in terms of bare functions. See #26118. Closes #25268