Metric structure on α →ᵤ β and α →ᵤ[𝔖] β for finite 𝔖 #
When β is a (pseudo, extended) metric space it is a uniform space, and therefore we may
consider the type α →ᵤ β of functions equipped with the topology of uniform convergence. The
natural (pseudo, extended) metric on this space is given by fun f g ↦ ⨆ x, edist (f x) (g x),
and this induces the existing uniformity. Unless β is a bounded space, this will not be a (pseudo)
metric space (except in the trivial case where α is empty).
When 𝔖 : Set (Set α) is a collection of subsets, we may equip the space of functions with the
(pseudo, extended) metric fun f g ↦ ⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x). However, this only induces
the pre-existing uniformity on α →ᵤ[𝔖] β if 𝔖 is finite, and hence we only have an instance in
that case. Nevertheless, this still covers the most important case, such as when 𝔖 is a singleton.
Furthermore, we note that this is essentially a mathematical obstruction, not a technical one:
indeed, the uniformity of α →ᵤ[𝔖] β is countably generated only when there is a sequence
t : ℕ → Finset (Set α) such that, for each n, t n ⊆ 𝔖, fun n ↦ Finset.sup (t n) is monotone
and for every s ∈ 𝔖, there is some n such that s ⊆ Finset.sup (t n) (see
UniformOnFun.isCountablyGenerated_uniformity). So, while the 𝔖 for which α →ᵤ[𝔖] β is
metrizable include some non-finite 𝔖, there are some 𝔖 which are not metrizable, and moreover,
it is only when 𝔖 is finite that ⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x) is a metric which induces the
uniformity.
There are a few advantages of equipping this space with this metric structure.
- A function
f : X → α →ᵤ βis Lipschitz in this metric if and only if for everya : αit is Lipschitz in the first variable with the same Lipschitz constant. - It provides a natural setting in which one can talk about the metrics on
α →ᵇ βor, whenαis compact,C(α, β), relative to their underlying bare functions.
Equations
- UniformFun.instEDist = { edist := fun (f g : UniformFun α β) => ⨆ (x : α), edist (UniformFun.toFun f x) (UniformFun.toFun g x) }
The natural EMetric structure on α →ᵤ β given by edist f g = ⨆ x, edist (f x) (g x).
Equations
- UniformFun.instPseudoEMetricSpace = { toEDist := UniformFun.instEDist, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, toUniformSpace := inferInstance, uniformity_edist := ⋯ }
If f : α → γ → β is a family of a functions, all of which are Lipschitz with the
same constant, then the family is uniformly equicontinuous.
If f : α → γ → β is a family of a functions, all of which are Lipschitz on s with the
same constant, then the family is uniformly equicontinuous on s.
Equations
- UniformFun.instPseudoMetricSpaceOfBoundedSpace = PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (f g : UniformFun α β) => ⨆ (x : α), dist (UniformFun.toFun f x) (UniformFun.toFun g x)) ⋯ ⋯
Let f : γ → α →ᵤ[𝔖] β. If for every s ∈ 𝔖 and for every c ∈ s, the function
fun x ↦ f x c is Lipschitz (with Lipschitz constant depending on s), then f is continuous.
Equations
- UniformOnFun.instEDistOfFiniteElemSet = { edist := fun (f g : UniformOnFun α β 𝔖) => ⨆ x ∈ ⋃₀ 𝔖, edist ((UniformOnFun.toFun 𝔖) f x) ((UniformOnFun.toFun 𝔖) g x) }
The natural EMetric structure on α →ᵤ[𝔖] β when 𝔖 is finite given by
edist f g = ⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x).
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.