Mathlib.Topology.MetricSpace.Completion

UniformSpace.Completion.instDist instance

: Dist (Completion α)

Full source

/-- The distance on the completion is obtained by extending the distance on the original space,
by uniform continuity. -/
instance : Dist (Completion α) :=
  ⟨Completion.extension₂ dist⟩

Distance Function on the Completion of a Metric Space

Informal description

The completion $\widehat{\alpha}$ of a metric space $\alpha$ is endowed with a distance function $\text{dist} : \widehat{\alpha} \times \widehat{\alpha} \to \mathbb{R}$, which is obtained by uniformly continuous extension of the distance function on $\alpha$. This distance function satisfies the properties of a pseudometric space, including reflexivity, symmetry, and the triangle inequality.

UniformSpace.Completion.uniformContinuous_dist theorem

: UniformContinuous fun p : Completion α × Completion α ↦ dist p.1 p.2

Full source

/-- The new distance is uniformly continuous. -/
protected theorem uniformContinuous_dist :
    UniformContinuous fun p : CompletionCompletion α × Completion α ↦ dist p.1 p.2 :=
  uniformContinuous_extension₂ dist

Uniform Continuity of the Distance Function on Metric Completion

Informal description

The distance function $\text{dist} \colon \widehat{\alpha} \times \widehat{\alpha} \to \mathbb{R}$ on the completion $\widehat{\alpha}$ of a metric space $\alpha$ is uniformly continuous, where $\widehat{\alpha}$ is equipped with the product uniform structure.

UniformSpace.Completion.continuous_dist theorem

 [TopologicalSpace β] {f g : β → Completion α} (hf : Continuous f) (hg : Continuous g) :
  Continuous fun x ↦ dist (f x) (g x)

Full source

/-- The new distance is continuous. -/
protected theorem continuous_dist [TopologicalSpace β] {f g : β → Completion α} (hf : Continuous f)
    (hg : Continuous g) : Continuous fun x ↦ dist (f x) (g x) :=
  Completion.uniformContinuous_dist.continuous.comp (hf.prodMk hg :)

Continuity of the Distance Function on the Completion of a Metric Space

Informal description

Let $\beta$ be a topological space and $f, g \colon \beta \to \widehat{\alpha}$ be continuous maps into the completion $\widehat{\alpha}$ of a metric space $\alpha$. Then the function $x \mapsto \text{dist}(f(x), g(x))$ is continuous on $\beta$.

UniformSpace.Completion.dist_eq theorem

(x y : α) : dist (x : Completion α) y = dist x y

Full source

/-- The new distance is an extension of the original distance. -/
@[simp]
protected theorem dist_eq (x y : α) : dist (x : Completion α) y = dist x y :=
  Completion.extension₂_coe_coe uniformContinuous_dist _ _

Distance Preservation in Metric Completion

Informal description

For any two points $x$ and $y$ in a metric space $\alpha$, the distance between their images in the completion $\widehat{\alpha}$ equals the original distance between $x$ and $y$, i.e., $\text{dist}(x, y) = \text{dist}(x, y)$ where $x$ and $y$ are identified with their canonical embeddings in $\widehat{\alpha}$.

UniformSpace.Completion.dist_self theorem

(x : Completion α) : dist x x = 0

Full source

protected theorem dist_self (x : Completion α) : dist x x = 0 := by
  refine induction_on x ?_ ?_
  · refine isClosed_eq ?_ continuous_const
    exact Completion.continuous_dist continuous_id continuous_id
  · intro a
    rw [Completion.dist_eq, dist_self]

Reflexivity of the Distance Function in Metric Completion

Informal description

For any point $x$ in the completion $\widehat{\alpha}$ of a metric space $\alpha$, the distance from $x$ to itself is zero, i.e., $\text{dist}(x, x) = 0$.

UniformSpace.Completion.dist_comm theorem

(x y : Completion α) : dist x y = dist y x

Full source

protected theorem dist_comm (x y : Completion α) : dist x y = dist y x := by
  refine induction_on₂ x y ?_ ?_
  · exact isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
        (Completion.continuous_dist continuous_snd continuous_fst)
  · intro a b
    rw [Completion.dist_eq, Completion.dist_eq, dist_comm]

Symmetry of Distance in Metric Completion

Informal description

For any two points $x$ and $y$ in the completion $\widehat{\alpha}$ of a metric space $\alpha$, the distance function is symmetric, i.e., $\text{dist}(x, y) = \text{dist}(y, x)$.

UniformSpace.Completion.dist_triangle theorem

(x y z : Completion α) : dist x z ≤ dist x y + dist y z

Full source

protected theorem dist_triangle (x y z : Completion α) : dist x z ≤ dist x y + dist y z := by
  refine induction_on₃ x y z ?_ ?_
  · refine isClosed_le ?_ (Continuous.add ?_ ?_) <;>
      apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
  · intro a b c
    rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]
    exact dist_triangle a b c

Triangle Inequality in the Completion of a Metric Space

Informal description

For any three points $x, y, z$ in the completion $\widehat{\alpha}$ of a metric space $\alpha$, the distance function satisfies the triangle inequality: \[ \text{dist}(x, z) \leq \text{dist}(x, y) + \text{dist}(y, z). \]

UniformSpace.Completion.mem_uniformity_dist theorem

 (s : Set (Completion α × Completion α)) : s ∈ 𝓤 (Completion α) ↔ ∃ ε > 0, ∀ {a b}, dist a b < ε → (a, b) ∈ s

Full source

/-- Elements of the uniformity (defined generally for completions) can be characterized in terms
of the distance. -/
protected theorem mem_uniformity_dist (s : Set (CompletionCompletion α × Completion α)) :
    s ∈ 𝓤 (Completion α)s ∈ 𝓤 (Completion α) ↔ ∃ ε > 0, ∀ {a b}, dist a b < ε → (a, b) ∈ s := by
  constructor
  · /- Start from an entourage `s`. It contains a closed entourage `t`. Its pullback in `α` is an
      entourage, so it contains an `ε`-neighborhood of the diagonal by definition of the entourages
      in metric spaces. Then `t` contains an `ε`-neighborhood of the diagonal in `Completion α`, as
      closed properties pass to the completion. -/
    intro hs
    rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩
    have A : { x : α × α | (↑x.1, ↑x.2) ∈ t }{ x : α × α | (↑x.1, ↑x.2) ∈ t } ∈ uniformity α :=
      uniformContinuous_def.1 (uniformContinuous_coe α) t ht
    rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩
    refine ⟨ε, εpos, @fun x y hxy ↦ ?_⟩
    have : ε ≤ dist x y ∨ (x, y) ∈ t := by
      refine induction_on₂ x y ?_ ?_
      · have : { x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t } =
               { p : Completion α × Completion α | ε ≤ dist p.1 p.2 }{ p : Completion α × Completion α | ε ≤ dist p.1 p.2 } ∪ t := by ext; simp
        rw [this]
        apply IsClosed.union _ tclosed
        exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
      · intro x y
        rw [Completion.dist_eq]
        by_cases h : ε ≤ dist x y
        · exact Or.inl h
        · have Z := hε (not_le.1 h)
          simp only [Set.mem_setOf_eq] at Z
          exact Or.inr Z
    simp only [not_le.mpr hxy, false_or, not_le] at this
    exact ts this
  · /- Start from a set `s` containing an ε-neighborhood of the diagonal in `Completion α`. To show
        that it is an entourage, we use the fact that `dist` is uniformly continuous on
        `Completion α × Completion α` (this is a general property of the extension of uniformly
        continuous functions). Therefore, the preimage of the ε-neighborhood of the diagonal in ℝ
        is an entourage in `Completion α × Completion α`. Massaging this property, it follows that
        the ε-neighborhood of the diagonal is an entourage in `Completion α`, and therefore this is
        also the case of `s`. -/
    rintro ⟨ε, εpos, hε⟩
    let r : Set (ℝℝ × ℝ) := { p | dist p.1 p.2 < ε }
    have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
    have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
    simp only [uniformity_prod_eq_prod, mem_prod_iff, exists_prop, Filter.mem_map,
      Set.mem_setOf_eq] at T
    rcases T with ⟨t1, ht1, t2, ht2, ht⟩
    refine mem_of_superset ht1 ?_
    have A : ∀ a b : Completion α, (a, b)(a, b) ∈ t1 → dist a b < ε := by
      intro a b hab
      have : ((a, b), (a, a))((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
      have I := ht this
      simp? [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] at I says
        simp only [Real.dist_eq, mem_setOf_eq, preimage_setOf_eq, Completion.dist_self,
          Completion.dist_comm, zero_sub, abs_neg, r] at I
      exact lt_of_le_of_lt (le_abs_self _) I
    show t1 ⊆ s
    rintro ⟨a, b⟩ hp
    have : dist a b < ε := A a b hp
    exact hε this

Characterization of Uniformity via Distance in Metric Completion

Informal description

For any set $s \subseteq \widehat{\alpha} \times \widehat{\alpha}$ in the completion $\widehat{\alpha}$ of a metric space $\alpha$, $s$ belongs to the uniformity filter $\mathfrak{U}(\widehat{\alpha})$ if and only if there exists $\varepsilon > 0$ such that for all $a, b \in \widehat{\alpha}$, if $\text{dist}(a, b) < \varepsilon$ then $(a, b) \in s$.

UniformSpace.Completion.uniformity_dist' theorem

: 𝓤 (Completion α) = ⨅ ε : { ε : ℝ // 0 < ε }, 𝓟 {p | dist p.1 p.2 < ε.val}

Full source

/-- Reformulate `Completion.mem_uniformity_dist` in terms that are suitable for the definition
of the metric space structure. -/
protected theorem uniformity_dist' :
    𝓤 (Completion α) = ⨅ ε : { ε : ℝ // 0 < ε }, 𝓟 { p | dist p.1 p.2 < ε.val } := by
  ext s; rw [mem_iInf_of_directed]
  · simp [Completion.mem_uniformity_dist, subset_def]
  · rintro ⟨r, hr⟩ ⟨p, hp⟩
    use ⟨min r p, lt_min hr hp⟩
    simp +contextual [lt_min_iff]

Uniformity Filter Characterization via Distance in Metric Completion

Informal description

The uniformity filter $\mathfrak{U}(\widehat{\alpha})$ on the completion $\widehat{\alpha}$ of a metric space $\alpha$ is equal to the infimum over all positive real numbers $\varepsilon$ of the principal filters generated by the sets $\{(x, y) \in \widehat{\alpha} \times \widehat{\alpha} \mid \text{dist}(x, y) < \varepsilon\}$.

UniformSpace.Completion.uniformity_dist theorem

: 𝓤 (Completion α) = ⨅ ε > 0, 𝓟 {p | dist p.1 p.2 < ε}

Full source

protected theorem uniformity_dist : 𝓤 (Completion α) = ⨅ ε > 0, 𝓟 { p | dist p.1 p.2 < ε } := by
  simpa [iInf_subtype] using @Completion.uniformity_dist' α _

Uniformity Filter Characterization via Distance in Metric Completion

Informal description

The uniformity filter $\mathfrak{U}(\widehat{\alpha})$ on the completion $\widehat{\alpha}$ of a metric space $\alpha$ is equal to the infimum over all positive real numbers $\varepsilon$ of the principal filters generated by the sets $\{(x, y) \in \widehat{\alpha} \times \widehat{\alpha} \mid \text{dist}(x, y) < \varepsilon\}$.

UniformSpace.Completion.instMetricSpace instance

: MetricSpace (Completion α)

Full source

/-- Metric space structure on the completion of a pseudo_metric space. -/
instance instMetricSpace : MetricSpace (Completion α) :=
  @MetricSpace.ofT0PseudoMetricSpace _
    { dist_self := Completion.dist_self
      dist_comm := Completion.dist_comm
      dist_triangle := Completion.dist_triangle
      dist := dist
      toUniformSpace := inferInstance
      uniformity_dist := Completion.uniformity_dist } _

Metric Space Structure on the Completion of a Metric Space

Informal description

The completion $\widehat{\alpha}$ of a metric space $\alpha$ inherits a metric space structure, where the distance function is extended from $\alpha$ to $\widehat{\alpha}$ and satisfies the metric space axioms. This extension preserves the original uniformity on $\widehat{\alpha}$.

UniformSpace.Completion.coe_isometry theorem

: Isometry ((↑) : α → Completion α)

Full source

/-- The embedding of a metric space in its completion is an isometry. -/
theorem coe_isometry : Isometry ((↑) : α → Completion α) :=
  Isometry.of_dist_eq Completion.dist_eq

Isometric Embedding of a Metric Space into its Completion

Informal description

The canonical embedding $(\uparrow) : \alpha \to \widehat{\alpha}$ from a metric space $\alpha$ to its completion $\widehat{\alpha}$ is an isometry, i.e., for any $x, y \in \alpha$, the distance between their images in $\widehat{\alpha}$ equals the original distance between $x$ and $y$: $\text{dist}(x, y) = \text{dist}(\uparrow x, \uparrow y)$.

UniformSpace.Completion.edist_eq theorem

(x y : α) : edist (x : Completion α) y = edist x y

Full source

@[simp]
protected theorem edist_eq (x y : α) : edist (x : Completion α) y = edist x y :=
  coe_isometry x y

Preservation of Extended Distance in Metric Space Completion

Informal description

For any two points $x$ and $y$ in a metric space $\alpha$, the extended distance between their images in the completion $\widehat{\alpha}$ equals the extended distance between $x$ and $y$ in $\alpha$, i.e., $\text{edist}(x, y) = \text{edist}(\uparrow x, \uparrow y)$.

UniformSpace.Completion.instIsBoundedSMul instance

{M} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [IsBoundedSMul M α] : IsBoundedSMul M (Completion α)

Full source

instance {M} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [IsBoundedSMul M α] :
    IsBoundedSMul M (Completion α) where
  dist_smul_pair' c x₁ x₂ := by
    induction x₁, x₂ using induction_on₂ with
    | hp =>
      exact isClosed_le
        ((continuous_fst.const_smul _).dist (continuous_snd.const_smul _))
        (continuous_const.mul (continuous_fst.dist continuous_snd))
    | ih x₁ x₂ =>
      rw [← coe_smul, ← coe_smul, Completion.dist_eq,  Completion.dist_eq]
      exact dist_smul_pair c x₁ x₂
  dist_pair_smul' c₁ c₂ x := by
    induction x using induction_on with
    | hp =>
      exact isClosed_le
        ((continuous_const_smul _).dist (continuous_const_smul _))
        (continuous_const.mul (continuous_id.dist continuous_const))
    | ih x =>
      rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq]
      exact dist_pair_smul c₁ c₂ x

Bounded Scalar Multiplication on the Completion of a Pseudometric Space

Informal description

For any pseudometric space $\alpha$ with a zero element and a scalar multiplication action by a pseudometric space $M$ with a zero element, if the scalar multiplication on $\alpha$ is bounded (i.e., satisfies the distance bounds for scalar multiplication), then the completion $\overline{\alpha}$ of $\alpha$ inherits a bounded scalar multiplication action by $M$.

LipschitzWith.completion_extension theorem

 [MetricSpace β] [CompleteSpace β] {f : α → β} {K : ℝ≥0} (h : LipschitzWith K f) :
  LipschitzWith K (Completion.extension f)

Full source

theorem LipschitzWith.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
    {K : ℝ≥0} (h : LipschitzWith K f) : LipschitzWith K (Completion.extension f) :=
  LipschitzWith.of_dist_le_mul fun x y => induction_on₂ x y
    (isClosed_le (by fun_prop) (by fun_prop)) <| by
      simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul

Lipschitz Property Preserved Under Completion Extension

Informal description

Let $\alpha$ and $\beta$ be metric spaces, with $\beta$ complete. For any $K \geq 0$ and any $K$-Lipschitz function $f \colon \alpha \to \beta$, the extension $\overline{f} \colon \widehat{\alpha} \to \beta$ of $f$ to the completion $\widehat{\alpha}$ of $\alpha$ is also $K$-Lipschitz.

LipschitzWith.completion_map theorem

[PseudoMetricSpace β] {f : α → β} {K : ℝ≥0} (h : LipschitzWith K f) : LipschitzWith K (Completion.map f)

Full source

theorem LipschitzWith.completion_map [PseudoMetricSpace β] {f : α → β} {K : ℝ≥0}
    (h : LipschitzWith K f) : LipschitzWith K (Completion.map f) :=
  one_mul K ▸ (coe_isometry.lipschitz.comp h).completion_extension

Lipschitz Property Preserved Under Completion Mapping

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f \colon \alpha \to \beta$ be a $K$-Lipschitz function for some $K \geq 0$. Then the induced map $\overline{f} \colon \widehat{\alpha} \to \widehat{\beta}$ between the completions of $\alpha$ and $\beta$ is also $K$-Lipschitz.

Isometry.completion_extension theorem

[MetricSpace β] [CompleteSpace β] {f : α → β} (h : Isometry f) : Isometry (Completion.extension f)

Full source

theorem Isometry.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
    (h : Isometry f) : Isometry (Completion.extension f) :=
  Isometry.of_dist_eq fun x y => induction_on₂ x y
    (isClosed_eq (by fun_prop) (by fun_prop)) fun _ _ ↦ by
      simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]

Isometry Extension to Metric Completion

Informal description

Let $\alpha$ and $\beta$ be metric spaces with $\beta$ complete, and let $f \colon \alpha \to \beta$ be an isometry. Then the extension $\overline{f} \colon \widehat{\alpha} \to \beta$ of $f$ to the completion $\widehat{\alpha}$ of $\alpha$ is also an isometry.

Isometry.completion_map theorem

[PseudoMetricSpace β] {f : α → β} (h : Isometry f) : Isometry (Completion.map f)

Full source

theorem Isometry.completion_map [PseudoMetricSpace β] {f : α → β}
    (h : Isometry f) : Isometry (Completion.map f) :=
  (coe_isometry.comp h).completion_extension

Isometry Lifting to Completions

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f \colon \alpha \to \beta$ be an isometry. Then the induced map $\overline{f} \colon \widehat{\alpha} \to \widehat{\beta}$ between the completions of $\alpha$ and $\beta$ is also an isometry.