Thickening and closed thickening

Stream: Is there code for X?

[Yaël Dillies]

Why are the API of docs#metric.thickening and docs#metric.cthickening different? In particular, is the following not true?

import topology.metric_space.hausdorff_distance

variables {X : Type*} [pseudo_metric_space X]

/-- A point in a metric space belongs to the (closed) `δ`-thickening of a subset `E` if and only if
it is at distance less than `δ` from some point of `E`. -/
lemma mem_cthickening_iff {δ : ℝ} (E : set X) (x : X) :
  x ∈ cthickening δ E ↔ ∃ z ∈ E, dist x z ≤ δ :=

[Yaël Dillies]

cc @Heather Macbeth, this is for #7288

[Yaël Dillies]

Okay, it indeed seems wrong...

[Yaël Dillies]

And I assume I'm missing an outside closure here too?

lemma cthickening_eq_bUnion_closed_ball {δ : ℝ} {s : set E} :
  cthickening δ s = ⋃ x ∈ s, closed_ball x δ :=
by { ext x, rw mem_bUnion_iff, exact mem_cthickening_iff E x, }

[Kalle Kytölä]

For the closed thickening you don't necessarily have a point at distance ≤ δthe thickening radius. It's an inf_dist (or inf_edist), so there are points at distance ≤ δ + εfor any ε > 0, but the lemma you state is not true in general.

[Yaël Dillies]

Yeah, I figured out...

[Yaël Dillies]

Btw #7288 is looking nicer and nicer! I'll PR exists_disjoint_thickenings tomorrow.

[Kalle Kytölä]

Concretely... The closed 37-thickening of the negative reals {x : ℝ | x < 0} contains 37, but no negative real is at distance ≤ 37from 37.

[Kalle Kytölä]

And the same example works to show the need for closure in the second lemma (as you observed). But sorry, I just arrived, and answered before reading two more lines to notice you had it figured out already in the messages after the first question... :laughter_tears:

[Yaël Dillies]

I wanted something like s + closed_ball 0 ε = cthickening ε s to be true. Do you think I should require s to be closed or take the closure of the LHS?

[Kalle Kytölä]

So as you observed, in that form it is not true. The open thickenings are much better behaved in this way. How to fix the "closed thickening / closed ball" case probably depends on the use case, but since the closed thickening is not generally well behaved with respect to this, are you sure it's what you want to do? (That said, both of your suggested fixes probably work. At least if you replace closed by compact. [EDIT: Sorry, closedness doesn't suffice but compactness indeed does. Below.])

[Yaël Dillies]

I don't need this, lemma, only the thickening version. I just wanted it for completeness.

[Kalle Kytölä]

I didn't originally include them, because the closed thickenings are not super well-behaved for things like this, and therefore I did not see those lemmas as very useful. (My most concrete use case is portmanteau theorem, and there I certainly will not use any such closed thickening thing, mosty only getting the closed thickenings as intersections of larger thickenings). But potentially under the is_compact s assumption it is worth including? The other approach is to wait for a use case and then decide.

[Yaël Dillies]

I guess I'll just wait, then.

[Kalle Kytölä]

(Just to correct one thing again, the closedness does not suffice, compactness is the assumption under which it does naturally hold.)

[Yaël Dillies]

Oh right, always the same funky counterexample. Was on my example sheet last term.

[Yaël Dillies]

One funny thing that I managed to prove is convex ℝ s → convex ℝ (cthickening ε s)

[Kalle Kytölä]

Perhaps a way to summarize these is to say that open thickenings behave well under unions, and closed thickenings behave well under intersections. (And under compactness additional miracles happen.) So maybe one should check if there are enough intersection lemmas for closed thickenings in the API. Or just wait for use cases to decide.

[Yaël Dillies]

Tomorrow happened #11458