Closure of a thickening

Stream: maths

[Yaël Dillies]

Is this true?

import analysis.normed_space.basic
import topology.metric_space.hausdorff_distance

open metric

variables {E : Type*} [normed_group E] [normed_space ℝ E] {δ : ℝ} {s : set E}

@[simp] lemma closure_thickening : closure (thickening δ s) = cthickening δ s :=
begin
  refine (closure_thickening_subset_cthickening _ _).antisymm (λ x hx, _),
  sorry
end

[Damiano Testa]

You may have to take the closure of s as well.

[Yaël Dillies]

No that can't be, because of docs#emetric.inf_edist_closure

[Yaël Dillies]

To be clear,

@[simp] lemma thickening_closure : thickening δ (closure s) = thickening δ s :=
by simp_rw [thickening, inf_edist_closure]

@[simp] lemma cthickening_closure : cthickening δ (closure s) = cthickening δ s :=
by simp_rw [cthickening, inf_edist_closure]

[Kevin Buzzard]

Surely this isn't true in general. What if the metric space is discrete? e.g. if d(a,b)=1 for a!=b isn't the 1-thickening of a set equal to the set and the 1-cthickening of a set is equal to everything.

[Damiano Testa]

I would have to look at the definitions, but is E allowed to be something pathological, like zmod 2?

[Yaël Dillies]

This is why I'm working in a real normed space, Kevin :grinning:

[Damiano Testa]

Oh, Kevin said the same!

[Kevin Buzzard]

Oh I see -- the point is that you want a real normed space -- yeah :-)

[Yaël Dillies]

The idea being that spheres in a normed space are thin.

[Kevin Buzzard]

Presumably you need much less, just something like if d(x,y)=1 then there's y_n with d(x,y_n)<1 and d(y_n,y)<1/n.

[Yaël Dillies]

Absolutely, but I don't know how to ask Lean for that.

[Kevin Buzzard]

Is there a math name for this? Do we care about this?

[Damiano Testa]

Would separable and no isolated points be what Kevin describes?

[Kevin Buzzard]

I guess in the normed space case you just take your point in s which is <= 1 from x and just draw a line through these two points and stick to this line.

[Yaël Dillies]

Through a long series of yak shaving PRs, this is useful for Hahn-Banach and Krein-Milman. The context is #13380.

[Kevin Buzzard]

aha, so it's worth thinking about. Is the concept of a perfect set relevant?

[Kevin Buzzard]

Yaël Dillies said:

Absolutely, but I don't know how to ask Lean for that.

I guess you don't just need it for 1, you need it for all positive reals.

[Damiano Testa]

It seems that perfect assumes also closed, though maybe it is not such a bad idea to have closed around anyway!

[Yaël Dillies]

I'm not sure perfect is exactly the right thing, but it certainly goes it the right direction.

[Damiano Testa]

docs#topological_space.separable_space seems to exist already.

[Kevin Buzzard]

Every countable space will be separable I guess, so Q with the discrete metric still causes problems.

[Damiano Testa]

You then only need the non-existence of isolated points, to avoid a single point being the only point in one of its neighbourhoods.

[Damiano Testa]

docs#real.punctured_nhds_module_ne_bot ?

[Floris van Doorn]

Damiano Testa said:

Would separable and no isolated points be what Kevin describes?

No, since I think Iic 0 ∪ Ici 1 (or $(-\infty, 0]\cup[1,\infty)$) satisfies your property, but not Kevin's, and Yael's requested lemma is false.

[Yaël Dillies]

Your link is broken, Damiano.

[Damiano Testa]

Yes, I am trying to fix it, but I am failing...

[Damiano Testa]

Updated to docs#real.punctured_nhds_module_ne_bot .

[Damiano Testa]

Floris, you are right: this should be assumed of s, not of E. And even so, I am not sure that your example will not get in the way.

[Yaël Dillies]

I'm not quite sure how to turn that into a statement about distances :thinking:

[Damiano Testa]

Anyway, I think that Kevin's statement is the way to go.

[Damiano Testa]

You can then try to leverage the existing API around separable_space and the punctured stuff.

[Yaël Dillies]

With perfect sets, you mean? Seems like we don't even have the definition, so this gonna be even more yak shaving :laughing:

[Damiano Testa]

I meant separable plus the condition that Kevin mentions.

[Damiano Testa]

(which you should assume on s, of course, since on E it might already exist, one way or another)

[Damiano Testa]

If you are going to use it for a separable space anyway, then fine. Otherwise, you may not need the implicit countable assumption on your dense subset.

[Damiano Testa]

So, just the existence of a dense set, which can approximately "slightly badly" every point!

[Kevin Buzzard]

How close is the assertion "if x != y and D=d(x.y) then for all n>=1 there's z with d(x,z)<D and d(z,y)<D/n" to the assertion "univ is a perfect subset of this metric space"?

[Kevin Buzzard]

Isn't that all you need?

[Damiano Testa]

It seems that you can replace s by closure s, so that would take care of the closure condition on perfect. Then you would need to verify that having no isolated points is preserved under taking closures (something that I have not actually thought about in weird contexts).

[Reid Barton]

I don't think "perfect" is the right concept. Floris already gave a counterexample above. It should be something more in the spirit of a geodesic space. But really, just do the proof for normed spaces.

[Yaël Dillies]

The proof turns out to be a one-liner using #13380 :big_smile:
See #13708