Euclidean distance on reals

Stream: Is there code for X?

[Kevin Buzzard]

An undergraduate asked me this in class today and I'm still stumped:

import Mathlib.Tactic
import Mathlib.Analysis.InnerProductSpace.EuclideanDist

example (x y : ℝ) : Euclidean.dist x y = |y - x| := by
  sorry

[Yaël Dillies]

I don't think that's true?

[Ruben Van de Velde]

That's because we don't know anything about Euclidean.distexcept that it's continuously differentiable

[Yaël Dillies]

docs#Euclidean.dist on a space E is defined using docs#toEuclidean, which is defined using an arbitrary continuous linear identification of E with Fin (dim E) → ℝ.

[Yaël Dillies]

There's no guarantee that this arbitrary identification preserves the distance between ℝ and Fin 1 → ℝ

[Riccardo Brasca]

Note that we have docs#Real.dist_eq, so it seems you should use dist.

[Ruben Van de Velde]

Sounds like https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/EuclideanDist.html needs a warning that you probably don't want it

[Antoine Chambert-Loir]

Yaël Dillies said:

docs#Euclidean.dist on a space E is defined using docs#toEuclidean, which is defined using an arbitrary continuous linear identification of E with Fin (dim E) → ℝ.

Exactly, and I don't believe it's reasonable to have such a function in the library, whose existence can only lead to misunderstanding.

[Antoine Chambert-Loir]

Ruben Van de Velde said:

Sounds like https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/EuclideanDist.html needs a warning that you probably don't want it

We lay want the existence of such a thing, that you can summon with obtain, without any guarantee of any compatibility.

[Yury G. Kudryashov]

AFAIR, I added this when I was working on the smooth partition of unity. Probably, we should remove it now (e.g., by using docs#toEuclidean instead).

[Antoine Chambert-Loir]

By using what instead? docs#toEuclidean is a fairly dangerous function.

[Yury G. Kudryashov]

Why is it dangerous?

[Kevin Buzzard]

because me and Jujian spent 5 minutes trying to prove the result at the top of this thread ;-)

[Yury G. Kudryashov]

I understand why Euclidean.dist is misleading. What's wrong with toEuclidean?

[Antoine Chambert-Loir]

Because that isomorphism depends on choices you can't predict. IMO, it should be written as an existential statement.

[Antoine Chambert-Loir]

But I see that this definition depends on the analogous docs#ContinuousLinearEquiv.ofFinrankEq about which I would raise the same criticism.

[Eric Wieser]

Antoine Chambert-Loir said:

Because that isomorphism depends on choices you can't predict. IMO, it should be written as an existential statement.

Using choose in the name might be a better compromise

[Eric Wieser]

Mathlib is full of functions that use choice to pick a somewhat arbitrary definition

[Antoine Chambert-Loir]

Using choose in the name might be useful indeed. On the other hand, what is the obstruction to using an existential statement with an obtain in a proof when no canonical stuff can be given? (Sometimes, I observed that the obtain tactic failed in a way I don't understand…)

[Eric Wieser]

The problem with using an existential is that you have to put every property you could think of under the same existential

[Eric Wieser]

(or you make some data-carrying object that means "has a canonical isomorphism with euclidean space", and have the existential unpack to that)

[Yury G. Kudryashov]

Sometimes ofFinrankEq is used to define non-canonical constants. Probably, they can be replaced by sInfs.