## Stream: Is there code for X?

### Topic: Should I be using has_dist vs abbreviation metric

#### Lars Ericson (Dec 07 2020 at 00:58):

In the following I have an abbreviation metric which says much the same thing as has_dist. Should I be using has_dist here somehow or is this OK? I am trying to define an example metric function prior to defining a metric space that uses it. I feel like I should be able to replace metric X in a function with has_dist X but it doesn't fit exactly:

import data.real.basic
import topology.metric_space.basic

-- Metric: α → α → ℝ

abbreviation metric (α: Type) := α → α → ℝ -- kind of recapitulates has_dist but has_dist α doesn't work as a function type

-- Example 1

abbreviation RealPoint : Type := ℝ × ℝ -- real points

noncomputable def d_taxicab : metric RealPoint := λ x y, (abs (x.1 - y.1)) + (abs (x.2 - y.2))

noncomputable def d_euclid : metric RealPoint := λ x y, real.sqrt ((x.1 - y.1)^2 + (x.2 - y.2)^2)

#check d_taxicab -- d_taxicab : metric RealPoint
#check d_euclid -- d_euclid : metric RealPoint


#### Yakov Pechersky (Dec 07 2020 at 01:05):

Providing a has_dist instance for some type, would allow you to say dist and have the function you provided in the has_dist statement be inferred. You will run into issues if you have two separate non-equal has_dist defined for the same type.

Can you give an example (that might not compile) of how you picture using has_dist instead?

#### Lars Ericson (Dec 07 2020 at 03:09):

I have

abbreviation metric (α: Type) := α → α → ℝ


and mathlib has

class has_dist (α : Type*) := (dist : α → α → ℝ)


They are declaring the same type for the same purpose.

I am creating a distance function such as

noncomputable def d_L1 : metric ℝ := λ x y, abs (x - y)


This goes into a metric_space such as

noncomputable def MES_L1 : metric_space ℝ :=
{ dist := d_L1,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }

#check MES_L1 -- MES_L1 : metric_space ℝ


It's a very small point but I am just asking whether there is a more mathlib-onic way of declaring d_L1 which uses has_dist so I don't have to create the redundant type abbreviation metric.

#### Johan Commelin (Dec 07 2020 at 06:07):

You should not be using abbreviation metric.
You should be using instances of the has_dist typeclass.
You should use those instances via the function dist (which assumes an instance of has_dist as one of its arguments).

#### Lars Ericson (Dec 07 2020 at 14:08):

Thank you @Johan Commelin . So the paradigm is to:

• Declare a type of functions which includes my distance function
• Provide that type with a has_dist, like this:
def bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] :
Type (max u v) :=
{f : α → β // continuous f ∧ ∃C, ∀x y:α, dist (f x) (f y) ≤ C}

local infixr  →ᵇ :25 := bounded_continuous_function

instance : has_dist (α →ᵇ β) :=
⟨λf g, Inf {C | 0 ≤ C ∧ ∀ x : α, dist (f x) (g x) ≤ C}⟩


Can you help me adapt the above example to the case where α = β = ℝ and d= λ x y, abs (x - y), so that the resulting d can be incorporated into the definition of a metric space?

#### Lars Ericson (Dec 08 2020 at 04:19):

OK I got it. Section 10.3. Here we go, please correct me if I'm wrong:

import data.real.basic
import topology.metric_space.basic

noncomputable def d_L1 := λ (x y : ℝ), abs (x - y)

noncomputable instance R_has_dist : has_dist ℝ := ⟨ d_L1 ⟩

noncomputable def MES_L1 : metric_space ℝ :=
{ dist := d_L1,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }

#check MES_L1 -- MES_L1 : metric_space ℝ


#### Lars Ericson (Dec 08 2020 at 13:52):

Done, revised to avoid instances:

mport data.real.basic
import topology.metric_space.basic

-- Example 1

noncomputable def d_L1 := λ (x y : ℝ), abs (x - y)

noncomputable def R_has_dist_L1 : has_dist ℝ := ⟨ d_L1 ⟩

noncomputable def MES_L1 : metric_space ℝ :=
{ dist := d_L1,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }

#check MES_L1 -- MES_L1 : metric_space ℝ

-- Example 2

noncomputable def d_L2 := λ (x y : ℝ), real.sqrt ((x - y)^2)

noncomputable def R_has_dist_l2 : has_dist ℝ := ⟨ d_L1 ⟩

noncomputable def MES_L2 : metric_space ℝ :=
{ dist := d_L2,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }

#check MES_L2 -- MES_L2 : metric_space ℝ

-- Example 3

abbreviation RealPoint : Type := ℝ × ℝ -- real points

noncomputable def d_taxicab := λ (x y : RealPoint), (abs (x.1 - y.1)) + (abs (x.2 - y.2))

noncomputable def RealPoint_has_dist_taxicab : has_dist RealPoint := ⟨ d_taxicab ⟩

noncomputable def MES_taxicab : metric_space RealPoint :=
{ dist := d_taxicab,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }

#check MES_taxicab -- MES_taxicab : metric_space RealPoint

-- Example 4

noncomputable def d_euclid  := λ (x y : RealPoint), real.sqrt ((x.1 - y.1)^2 + (x.2 - y.2)^2)

noncomputable def RealPoint_has_dist_euclid : has_dist RealPoint := ⟨ d_taxicab ⟩

noncomputable def MES_euclid: metric_space RealPoint :=
{ dist := d_euclid,
dist_self := sorry,
eq_of_dist_eq_zero := sorry,
dist_comm := sorry,
dist_triangle := sorry }

#check MES_euclid -- MES_taxicab : metric_space RealPoint


#### Eric Wieser (Dec 08 2020 at 14:08):

Typo: R_has_dist_l2 : has_dist ℝ := ⟨ d_L1 ⟩ should be R_has_dist_l2 : has_dist ℝ := ⟨ d_L2 ⟩

#### Lars Ericson (Dec 08 2020 at 14:58):

Thanks, fixed.

Last updated: May 16 2021 at 05:21 UTC