Extended metric spaces

Further results about extended metric spaces.

theorem edist_le_Ico_sum_edist {α : Type u} [PseudoEMetricSpace α] (f : ℕ → α) {m : ℕ} {n : ℕ} (h : m ≤ n) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))

The triangle (polygon) inequality for sequences of points; Finset.Ico version.

theorem edist_le_range_sum_edist {α : Type u} [PseudoEMetricSpace α] (f : ℕ → α) (n : ℕ) : edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1))

The triangle (polygon) inequality for sequences of points; Finset.range version.

theorem edist_le_Ico_sum_of_edist_le {α : Type u} [PseudoEMetricSpace α] {f : ℕ → α} {m : ℕ} {n : ℕ} (hmn : m ≤ n) {d : ℕ → ENNReal} (hd : ∀ {k : ℕ}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i

A version of edist_le_Ico_sum_edist with each intermediate distance replaced with an upper estimate.

theorem edist_le_range_sum_of_edist_le {α : Type u} [PseudoEMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ENNReal} (hd : ∀ {k : ℕ}, k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i

A version of edist_le_range_sum_edist with each intermediate distance replaced with an upper estimate.

theorem EMetric.uniformInducing_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : UniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

theorem EMetric.isUniformEmbedding_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

ε-δ characterization of uniform embeddings on pseudoemetric spaces

@[deprecated EMetric.isUniformEmbedding_iff]

theorem EMetric.uniformEmbedding_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Alias of EMetric.isUniformEmbedding_iff.

---

ε-δ characterization of uniform embeddings on pseudoemetric spaces

theorem EMetric.controlled_of_isUniformEmbedding {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : IsUniformEmbedding f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

If a map between pseudoemetric spaces is a uniform embedding then the edistance between f x and f y is controlled in terms of the distance between x and y.

In fact, this lemma holds for a UniformInducing map. TODO: generalize?

@[deprecated EMetric.controlled_of_isUniformEmbedding]

theorem EMetric.controlled_of_uniformEmbedding {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : IsUniformEmbedding f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Alias of EMetric.controlled_of_isUniformEmbedding.

---

If a map between pseudoemetric spaces is a uniform embedding then the edistance between f x and f y is controlled in terms of the distance between x and y.

In fact, this lemma holds for a UniformInducing map. TODO: generalize?

theorem EMetric.cauchy_iff {α : Type u} [PseudoEMetricSpace α] {f : Filter α} : Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

ε-δ characterization of Cauchy sequences on pseudoemetric spaces

theorem EMetric.complete_of_convergent_controlled_sequences {α : Type u} [PseudoEMetricSpace α] (B : ℕ → ENNReal) (hB : ∀ (n : ℕ), 0 < B n) (H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ (x : α), Filter.Tendsto u Filter.atTop (nhds x)) : CompleteSpace α

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form edist (u n) (u m) < B N for all n m ≥ N are converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to 0, which makes it possible to use arguments of converging series, while this is impossible to do in general for arbitrary Cauchy sequences.

theorem EMetric.complete_of_cauchySeq_tendsto {α : Type u} [PseudoEMetricSpace α] : (∀ (u : ℕ → α), CauchySeq u → ∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α

A sequentially complete pseudoemetric space is complete.

theorem EMetric.tendstoLocallyUniformlyOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Expressing locally uniform convergence on a set using edist.

theorem EMetric.tendstoUniformlyOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Expressing uniform convergence on a set using edist.

theorem EMetric.tendstoLocallyUniformly_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Expressing locally uniform convergence using edist.

theorem EMetric.tendstoUniformly_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε

Expressing uniform convergence using edist.

theorem EMetric.inseparable_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} : Inseparable x y ↔ edist x y = 0

theorem Inseparable.edist_eq_zero {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} : Inseparable x y → edist x y = 0

Alias of the forward direction of EMetric.inseparable_iff.

theorem EMetric.cauchySeq_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (u m) (u n) < ε

In a pseudoemetric space, Cauchy sequences are characterized by the fact that, eventually, the pseudoedistance between its elements is arbitrarily small

theorem EMetric.cauchySeq_iff' {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, edist (u n) (u N) < ε

A variation around the emetric characterization of Cauchy sequences

theorem EMetric.cauchySeq_iff_NNReal {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ (ε : NNReal), 0 < ε → ∃ (N : β), ∀ (n : β), N ≤ n → edist (u n) (u N) < ↑ε

A variation of the emetric characterization of Cauchy sequences that deals with ℝ≥0 upper bounds.

theorem EMetric.totallyBounded_iff {α : Type u} [PseudoEMetricSpace α] {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε

theorem EMetric.totallyBounded_iff' {α : Type u} [PseudoEMetricSpace α] {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε

theorem EMetric.subset_countable_closure_of_compact {α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : IsCompact s) : ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

A compact set in a pseudo emetric space is separable, i.e., it is a subset of the closure of a countable set.

@[instance 90]

instance EMetric.secondCountable_of_sigmaCompact (α : Type u) [PseudoEMetricSpace α] [SigmaCompactSpace α] : SecondCountableTopology α

A sigma compact pseudo emetric space has second countable topology.

Equations

• ⋯ = ⋯

theorem EMetric.secondCountable_of_almost_dense_set {α : Type u} [PseudoEMetricSpace α] (hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = Set.univ) : SecondCountableTopology α

@[instance 100]

instance EMetricSpace.instT0Space {γ : Type w} [EMetricSpace γ] : T0Space γ

An emetric space is separated

Equations

• ⋯ = ⋯

theorem EMetric.isUniformEmbedding_iff' {β : Type v} {γ : Type w} [EMetricSpace γ] [EMetricSpace β] {f : γ → β} : IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ

A map between emetric spaces is a uniform embedding if and only if the edistance between f x and f y is controlled in terms of the distance between x and y and conversely.

@[deprecated EMetric.isUniformEmbedding_iff']

theorem EMetric.uniformEmbedding_iff' {β : Type v} {γ : Type w} [EMetricSpace γ] [EMetricSpace β] {f : γ → β} : IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ

Alias of EMetric.isUniformEmbedding_iff'.

---

A map between emetric spaces is a uniform embedding if and only if the edistance between f x and f y is controlled in terms of the distance between x and y and conversely.

@[reducible, inline]

abbrev EMetricSpace.ofT0PseudoEMetricSpace (α : Type u_2) [PseudoEMetricSpace α] [T0Space α] : EMetricSpace α

If a PseudoEMetricSpace is a T₀ space, then it is an EMetricSpace.

Equations

• EMetricSpace.ofT0PseudoEMetricSpace α = EMetricSpace.mk ⋯

instance Prod.emetricSpaceMax {β : Type v} {γ : Type w} [EMetricSpace γ] [EMetricSpace β] : EMetricSpace (γ × β)

The product of two emetric spaces, with the max distance, is an extended metric spaces. We make sure that the uniform structure thus constructed is the one corresponding to the product of uniform spaces, to avoid diamond problems.

Equations

• Prod.emetricSpaceMax = EMetricSpace.ofT0PseudoEMetricSpace (γ × β)

theorem EMetric.countable_closure_of_compact {γ : Type w} [EMetricSpace γ] {s : Set γ} (hs : IsCompact s) : ∃ t ⊆ s, t.Countable ∧ s = closure t

A compact set in an emetric space is separable, i.e., it is the closure of a countable set.

Separation quotient

instance instEDistSeparationQuotient {X : Type u_1} [PseudoEMetricSpace X] : EDist (SeparationQuotient X)

Equations

• instEDistSeparationQuotient = { edist := SeparationQuotient.lift₂ edist ⋯ }

@[simp]

theorem SeparationQuotient.edist_mk {X : Type u_1} [PseudoEMetricSpace X] (x : X) (y : X) : edist (SeparationQuotient.mk x) (SeparationQuotient.mk y) = edist x y

instance instEMetricSpaceSeparationQuotient {X : Type u_1} [PseudoEMetricSpace X] : EMetricSpace (SeparationQuotient X)

Equations

• instEMetricSpaceSeparationQuotient = EMetricSpace.ofT0PseudoEMetricSpace (SeparationQuotient X)