# Zulip Chat Archive

## 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