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.

1. A function f : X → α →ᵤ β is Lipschitz in this metric if and only if for every a : α it is Lipschitz in the first variable with the same Lipschitz constant.
2. 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.

noncomputable instance UniformFun.instEDist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace β] : EDist (UniformFun α β)

theorem UniformFun.edist_def {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace β] (f g : UniformFun α β) : edist f g = ⨆ (x : α), edist (toFun f x) (toFun g x)

theorem UniformFun.edist_le {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace β] {f g : UniformFun α β} {C : ENNReal} : edist f g ≤ C ↔ ∀ (x : α), edist (toFun f x) (toFun g x) ≤ C

noncomputable instance UniformFun.instPseudoEMetricSpace {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace β] : PseudoEMetricSpace (UniformFun α β)

The natural EMetric structure on α →ᵤ β given by edist f g = ⨆ x, edist (f x) (g x).

noncomputable instance UniformFun.instEMetricSpace {α : Type u_1} {β : Type u_4} [EMetricSpace β] : EMetricSpace (UniformFun α β)

theorem UniformFun.lipschitzWith_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → UniformFun α β} {K : NNReal} : LipschitzWith K f ↔ ∀ (c : α), LipschitzWith K fun (x : γ) => toFun (f x) c

theorem UniformFun.lipschitzWith_ofFun_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → α → β} {K : NNReal} : (LipschitzWith K fun (x : γ) => ofFun (f x)) ↔ ∀ (c : α), LipschitzWith K fun (x : γ) => f x c

theorem LipschitzWith.uniformEquicontinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] (f : α → γ → β) (K : NNReal) (h : ∀ (c : α), LipschitzWith K (f c)) : UniformEquicontinuous f

If f : α → γ → β is a family of a functions, all of which are Lipschitz with the same constant, then the family is uniformly equicontinuous.

theorem UniformFun.lipschitzOnWith_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → UniformFun α β} {K : NNReal} {s : Set γ} : LipschitzOnWith K f s ↔ ∀ (c : α), LipschitzOnWith K (fun (x : γ) => toFun (f x) c) s

theorem UniformFun.lipschitzOnWith_ofFun_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] {f : γ → α → β} {K : NNReal} {s : Set γ} : LipschitzOnWith K (fun (x : γ) => ofFun (f x)) s ↔ ∀ (c : α), LipschitzOnWith K (fun (x : γ) => f x c) s

theorem LipschitzOnWith.uniformEquicontinuousOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] [PseudoEMetricSpace β] (f : α → γ → β) (K : NNReal) {s : Set γ} (h : ∀ (c : α), LipschitzOnWith K (f c) s) : UniformEquicontinuousOn f s

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.

theorem UniformFun.edist_eval_le {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace β] {f g : UniformFun α β} {x : α} : edist (toFun f x) (toFun g x) ≤ edist f g

theorem UniformFun.lipschitzWith_eval {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace β] (x : α) : LipschitzWith 1 fun (f : UniformFun α β) => toFun f x

noncomputable instance UniformFun.instPseudoMetricSpaceOfBoundedSpace {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [BoundedSpace β] : PseudoMetricSpace (UniformFun α β)

theorem UniformFun.dist_def {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [BoundedSpace β] (f g : UniformFun α β) : dist f g = ⨆ (x : α), dist (toFun f x) (toFun g x)

theorem UniformFun.dist_le {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [BoundedSpace β] {f g : UniformFun α β} {C : ℝ} (hC : 0 ≤ C) : dist f g ≤ C ↔ ∀ (x : α), dist (toFun f x) (toFun g x) ≤ C

instance UniformFun.instBoundedSpace {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [BoundedSpace β] : BoundedSpace (UniformFun α β)

noncomputable instance UniformFun.instMetricSpaceOfBoundedSpace {α : Type u_1} {β : Type u_4} [MetricSpace β] [BoundedSpace β] : MetricSpace (UniformFun α β)

theorem UniformFun.isometry_ofFun_boundedContinuousFunction {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [TopologicalSpace α] : Isometry (⇑ofFun ∘ DFunLike.coe)

theorem UniformFun.isometry_ofFun_continuousMap {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [TopologicalSpace α] [CompactSpace α] : Isometry (⇑ofFun ∘ DFunLike.coe)

theorem UniformFun.edist_continuousMapMk {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [TopologicalSpace α] [CompactSpace α] {f g : UniformFun α β} (hf : Continuous (toFun f)) (hg : Continuous (toFun g)) : edist { toFun := toFun f, continuous_toFun := hf } { toFun := toFun g, continuous_toFun := hg } = edist f g

theorem UniformOnFun.continuous_of_forall_lipschitzWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] {𝔖 : Set (Set α)} [PseudoEMetricSpace β] {f : γ → UniformOnFun α β 𝔖} (K : Set α → NNReal) (h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun (x : γ) => (toFun 𝔖) (f x) c) : Continuous f

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.

noncomputable instance UniformOnFun.instEDistOfFiniteElemSet {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] : EDist (UniformOnFun α β 𝔖)

theorem UniformOnFun.edist_def {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] (f g : UniformOnFun α β 𝔖) : edist f g = ⨆ x ∈ ⋃₀ 𝔖, edist ((toFun 𝔖) f x) ((toFun 𝔖) g x)

theorem UniformOnFun.edist_def' {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] (f g : UniformOnFun α β 𝔖) : edist f g = ⨆ s ∈ 𝔖, ⨆ x ∈ s, edist ((toFun 𝔖) f x) ((toFun 𝔖) g x)

theorem UniformOnFun.edist_eq_restrict_sUnion {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] {f g : UniformOnFun α β 𝔖} : edist f g = edist (UniformFun.ofFun ((⋃₀ 𝔖).restrict ((toFun 𝔖) f))) (UniformFun.ofFun ((⋃₀ 𝔖).restrict ((toFun 𝔖) g)))

theorem UniformOnFun.edist_eq_pi_restrict {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Fintype ↑𝔖] {f g : UniformOnFun α β 𝔖} : edist f g = edist (fun (s : ↑𝔖) => UniformFun.ofFun ((↑s).restrict ((toFun 𝔖) f))) fun (s : ↑𝔖) => UniformFun.ofFun ((↑s).restrict ((toFun 𝔖) g))

noncomputable instance UniformOnFun.instPseudoEMetricSpace {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] : PseudoEMetricSpace (UniformOnFun α β 𝔖)

The natural EMetric structure on α →ᵤ[𝔖] β when 𝔖 is finite given by edist f g = ⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x).

theorem UniformOnFun.edist_le {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] {f g : UniformOnFun α β 𝔖} {C : ENNReal} : edist f g ≤ C ↔ ∀ x ∈ ⋃₀ 𝔖, edist ((toFun 𝔖) f x) ((toFun 𝔖) g x) ≤ C

theorem UniformOnFun.lipschitzWith_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] {f : γ → UniformOnFun α β 𝔖} {K : NNReal} : LipschitzWith K f ↔ ∀ c ∈ ⋃₀ 𝔖, LipschitzWith K fun (x : γ) => (toFun 𝔖) (f x) c

theorem UniformOnFun.lipschitzOnWith_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace γ] {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] {f : γ → UniformOnFun α β 𝔖} {K : NNReal} {s : Set γ} : LipschitzOnWith K f s ↔ ∀ c ∈ ⋃₀ 𝔖, LipschitzOnWith K (fun (x : γ) => (toFun 𝔖) (f x) c) s

theorem UniformOnFun.edist_eval_le {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] {f g : UniformOnFun α β 𝔖} {x : α} (hx : x ∈ ⋃₀ 𝔖) : edist ((toFun 𝔖) f x) ((toFun 𝔖) g x) ≤ edist f g

theorem UniformOnFun.lipschitzWith_eval {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] {x : α} (hx : x ∈ ⋃₀ 𝔖) : LipschitzWith 1 fun (f : UniformOnFun α β 𝔖) => (toFun 𝔖) f x

theorem UniformOnFun.lipschitzWith_one_ofFun_toFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] : LipschitzWith 1 (⇑(ofFun 𝔖) ∘ ⇑UniformFun.toFun)

theorem UniformOnFun.lipschitzWith_one_ofFun_toFun' {α : Type u_1} {β : Type u_2} {𝔖 𝔗 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] [Finite ↑𝔗] (h : ⋃₀ 𝔖 ⊆ ⋃₀ 𝔗) : LipschitzWith 1 (⇑(ofFun 𝔖) ∘ ⇑(toFun 𝔗))

theorem UniformOnFun.lipschitzWith_restrict {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] (s : Set α) (hs : s ∈ 𝔖) : LipschitzWith 1 (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖))

theorem UniformOnFun.isometry_restrict {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace β] (s : Set α) : Isometry (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun {s}))

noncomputable instance UniformOnFun.instPseudoMetricSpaceOfBoundedSpace {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Finite ↑𝔖] [PseudoMetricSpace β] [BoundedSpace β] : PseudoMetricSpace (UniformOnFun α β 𝔖)

instance UniformOnFun.instBoundedSpace {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Finite ↑𝔖] [PseudoMetricSpace β] [BoundedSpace β] : BoundedSpace (UniformOnFun α β 𝔖)

theorem UniformOnFun.edist_continuousRestrict {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Finite ↑𝔖] [PseudoMetricSpace β] [TopologicalSpace α] {f g : UniformOnFun α β 𝔖} [CompactSpace ↑(⋃₀ 𝔖)] (hf : ContinuousOn ((toFun 𝔖) f) (⋃₀ 𝔖)) (hg : ContinuousOn ((toFun 𝔖) g) (⋃₀ 𝔖)) : edist { toFun := (⋃₀ 𝔖).restrict ((toFun 𝔖) f), continuous_toFun := ⋯ } { toFun := (⋃₀ 𝔖).restrict ((toFun 𝔖) g), continuous_toFun := ⋯ } = edist f g

theorem UniformOnFun.edist_continuousRestrict_of_singleton {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] [TopologicalSpace α] {s : Set α} {f g : UniformOnFun α β {s}} [CompactSpace ↑s] (hf : ContinuousOn ((toFun {s}) f) s) (hg : ContinuousOn ((toFun {s}) g) s) : edist { toFun := s.restrict ((toFun {s}) f), continuous_toFun := ⋯ } { toFun := s.restrict ((toFun {s}) g), continuous_toFun := ⋯ } = edist f g