mathlib docs: topology.metric_space.gromov_hausdorff

source

def Gromov_Hausdorff.candidates (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

set (prod_space_fun α β)

The set of functions on α ⊕ β that are candidates distances to realize the minimum of the Hausdorff distances between α and β in a coupling

Equations

Gromov_Hausdorff.candidates α β = {f : prod_space_fun α β | (((((∀ (x y : α), f (sum.inl x, sum.inl y) = has_dist.dist x y) ∧ ∀ (x y : β), f (sum.inr x, sum.inr y) = has_dist.dist x y) ∧ ∀ (x y : α ⊕ β), f (x, y) = f (y, x)) ∧ ∀ (x y z : α ⊕ β), f (x, z) ≤ f (x, y) + f (y, z)) ∧ ∀ (x : α ⊕ β), f (x, x) = 0) ∧ ∀ (x y : α ⊕ β), f (x, y) ≤ ↑(max_var α β)}

source

def Gromov_Hausdorff.candidates_b_of_candidates {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] (f : prod_space_fun α β) :

f ∈ Gromov_Hausdorff.candidates α β → Cb α β

candidates give rise to elements of bounded_continuous_functions

Equations

Gromov_Hausdorff.candidates_b_of_candidates f fA = bounded_continuous_function.mk_of_compact f _

source

theorem Gromov_Hausdorff.candidates_b_of_candidates_mem {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] (f : prod_space_fun α β) (fA : f ∈ Gromov_Hausdorff.candidates α β) :

Gromov_Hausdorff.candidates_b_of_candidates f fA ∈ candidates_b α β

source

def Gromov_Hausdorff.candidates_b_dist (α : Type u) (β : Type v) [metric_space α] [compact_space α] [inhabited α] [metric_space β] [compact_space β] [inhabited β] :

Cb α β

Equations

Gromov_Hausdorff.candidates_b_dist α β = Gromov_Hausdorff.candidates_b_of_candidates (λ (p : (α ⊕ β) × (α ⊕ β)), has_dist.dist p.fst p.snd) _

source

theorem Gromov_Hausdorff.candidates_b_dist_mem_candidates_b {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

Gromov_Hausdorff.candidates_b_dist α β ∈ candidates_b α β

source

def Gromov_Hausdorff.HD {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

Cb α β → ℝ

We will then choose the candidate minimizing the Hausdorff distance. Except that we are not in a metric space setting, so we need to define our custom version of Hausdorff distance, called HD, and prove its basic properties.

Equations

Gromov_Hausdorff.HD f = max (⨆ (x : α), ⨅ (y : β), ⇑f (sum.inl x, sum.inr y)) (⨆ (y : β), ⨅ (x : α), ⇑f (sum.inl x, sum.inr y))

source

theorem Gromov_Hausdorff.HD_below_aux1 {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] {f : Cb α β} (C : ℝ) {x : α} :

bdd_below (set.range (λ (y : β), ⇑f (sum.inl x, sum.inr y) + C))

source

theorem Gromov_Hausdorff.HD_below_aux2 {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] {f : Cb α β} (C : ℝ) {y : β} :

bdd_below (set.range (λ (x : α), ⇑f (sum.inl x, sum.inr y) + C))

source

theorem Gromov_Hausdorff.HD_candidates_b_dist_le {α : Type u} {β : Type v} [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

Gromov_Hausdorff.HD (Gromov_Hausdorff.candidates_b_dist α β) ≤ metric.diam set.univ + 1 + metric.diam set.univ

Explicit bound on HD (dist). This means that when looking for minimizers it will be sufficient to look for functions with HD(f) bounded by this bound.

source

def Gromov_Hausdorff.premetric_optimal_GH_dist (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

premetric_space (α ⊕ β)

With the optimal candidate, construct a premetric space structure on α ⊕ β, on which the predistance is given by the candidate. Then, we will identify points at 0 predistance to obtain a genuine metric space

Equations

Gromov_Hausdorff.premetric_optimal_GH_dist α β = {to_has_dist := {dist := λ (p q : α ⊕ β), ⇑(optimal_GH_dist α β) (p, q)}, dist_self := _, dist_comm := _, dist_triangle := _}

source

def Gromov_Hausdorff.optimal_GH_coupling (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

Type (max u v)

A metric space which realizes the optimal coupling between α and β

Equations

Gromov_Hausdorff.optimal_GH_coupling α β = premetric.metric_quot (α ⊕ β)

source

@[instance]

def Gromov_Hausdorff.optimal_GH_coupling.metric_space (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

metric_space (Gromov_Hausdorff.optimal_GH_coupling α β)

source

def Gromov_Hausdorff.optimal_GH_injl (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

α → Gromov_Hausdorff.optimal_GH_coupling α β

Injection of α in the optimal coupling between α and β

Equations

Gromov_Hausdorff.optimal_GH_injl α β x = ⟦sum.inl x⟧

source

theorem Gromov_Hausdorff.isometry_optimal_GH_injl (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

isometry (Gromov_Hausdorff.optimal_GH_injl α β)

The injection of α in the optimal coupling between α and β is an isometry.

source

def Gromov_Hausdorff.optimal_GH_injr (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

β → Gromov_Hausdorff.optimal_GH_coupling α β

Injection of β in the optimal coupling between α and β

Equations

Gromov_Hausdorff.optimal_GH_injr α β y = ⟦sum.inr y⟧

source

theorem Gromov_Hausdorff.isometry_optimal_GH_injr (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

isometry (Gromov_Hausdorff.optimal_GH_injr α β)

The injection of β in the optimal coupling between α and β is an isometry.

source

@[instance]

def Gromov_Hausdorff.compact_space_optimal_GH_coupling (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] :

compact_space (Gromov_Hausdorff.optimal_GH_coupling α β)

The optimal coupling between two compact spaces α and β is still a compact space

Equations

_ = _

source

theorem Gromov_Hausdorff.Hausdorff_dist_optimal_le_HD (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β] {f : Cb α β} :

f ∈ candidates_b α β → metric.Hausdorff_dist (set.range (Gromov_Hausdorff.optimal_GH_injl α β)) (set.range (Gromov_Hausdorff.optimal_GH_injr α β)) ≤ Gromov_Hausdorff.HD f

For any candidate f, HD(f) is larger than or equal to the Hausdorff distance in the optimal coupling. This follows from the fact that HD of the optimal candidate is exactly the Hausdorff distance in the optimal coupling, although we only prove here the inequality we need.

mathlib documentation

topology.metric_space.gromov_hausdorff_realized

General documentation

Additional documentation

Library

mathlib documentation

topology.​metric_space.​gromov_hausdorff_realized

General documentation

Additional documentation

Library

topology.metric_space.gromov_hausdorff_realized