Realizing the Hausdorff distance

Stream: Is there code for X?

[Yaël Dillies]

Do we know that docs#emetric.Hausdorff_edist is realized when the two sets are (seq) compact? I'm pretty sure this is true. Context is #11458

[Yury G. Kudryashov]

I can't find it (it should be easy to prove for compact sets). @Sebastien Gouezel ?

[Yaël Dillies]

Btw Sébastien I'm proving a bunch of ball lemmas in #11458 and I would appreciate some help in finishing off stuff like

import topology.metric_space.hausdorff_distance

open metric

variables {ε δ : ℝ}

@[simp] lemma thickening_thickening (hε : 0 < ε) (hδ : 0 < δ) (s : set E) :
  thickening ε (thickening δ s) = thickening (ε + δ) s := sorry

@[simp] lemma thickening_cthickening (hε : 0 < ε) (hδ : 0 ≤ δ) (s : set E) :
  thickening ε (cthickening δ s) = thickening (ε + δ) s := sorry

@[simp] lemma cthickening_thickening (hε : 0 ≤ ε) (hδ : 0 < δ) (s : set E) :
  cthickening ε (thickening δ s) = cthickening (ε + δ) s := sorry

@[simp] lemma cthickening_cthickening (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : set E) :
  cthickening ε (cthickening δ s) = cthickening (ε + δ) s := sorry

[Yaël Dillies]

One inclusion is obvious, but is the other one true? If a and b are at distance < ε + δ, is there a c at distance < ε from a and < δ from b? This hurts my brain...

[Junyan Xu]

Yeah the reverse inequality should not always hold. If you thicken $\{0\}\subset\mathbb{Z}$ by 3/4 you get {0} again, the same if you do it twice, but if you thicken by 3/2 you get {-1,0,1}.

[Yaël Dillies]

So this is wrong as well, right? ball a ε + ball b δ = ball (a + b) (ε + δ)
What's the correct generality to salvage my results? I want them over a $\R$-module anyway.

[Yaël Dillies]

Surely normed_field is enough?

[Yaël Dillies]

Oh, better, module ℝ E. How does that sound?

[Junyan Xu]

module ℝ E should work. p-adic fields are problematic as the norm function takes discrete values.

[Yaël Dillies]

I swear module ℚ E should be enough, but I don't know which one is more practical.

[Junyan Xu]

Well p-adic fields are Q-modules; it depends on what norm you put on E.

[Junyan Xu]

(Not just discrete values; due to the nonarchimedean triangle inequality, thickening the r-ball by r you get the r-ball again (for p-adic fields).)
(the nonarchimedean triangle inequality says ||x+y|| <= max(||x||,||y||))

[Yaël Dillies]

What are those spaces and how can I conjure them

[Junyan Xu]

so I think module ℝ E is not enough and you need normed_space which says how the smul interacts with the norm.

[Junyan Xu]

I think normed_space ℚ E works for the two lemmas starting with thickening but not the two starting with cthickening (which should work however if E is complete). ℚ can be replaced with any normed_field with values of norm function dense in ℝ, I believe. normed_space ℝ Eshould work for all four.

[Junyan Xu]

Yaël Dillies said:

What are those spaces and how can I conjure them

The field of p-adic numbers is defined to be the completion of ℚ equipped with the norm ||a/b|| = base^(v(b)-v(a)), where v(a) is the number of times p divides a, for a in ℤ, and base > 1 a real number usually taken to be p. (ℚ equipped with that norm is already a field satisfying the nonarchimedean triangle inequality, we don't need completion for this purpose.)

[Junyan Xu]

You may want to read https://en.wikipedia.org/wiki/Ostrowski%27s_theorem (do we have this in mathlib?)

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Ostrowski.20theorems.20formalized.20in.20Lean.203 but I don't think it made it to mathlib

[Yury G. Kudryashov]

For a proof with normed_space, you can use docs#normed_space.sphere_nonempty