[Merged by Bors] - feat(topology/metric_space/hausdorff_distance): add definition and lemmas about closed thickenings of subsets

[kkytola]

Add definition and basic API about closed thickenings of subsets in metric spaces, in preparation for the portmanteau theorem on characterizations of weak convergence of Borel probability measures.

---

This is a continuation of a (rather independent) part of my attempt to PR a proof of the portmanteau theorem https://github.com/kkytola/lean_portmanteau. Specifically it is intended as an improved and cleaned up version of a manageable size chunck of the file https://github.com/kkytola/lean_portmanteau/blob/main/portmanteau_metric_lemmas.lean.

For portmanteau purposes, this PR still needs to be followed up by some further API, in particular continuous approximations of indicator functions of closed sets, and crucially, the countability of thickening-radii such that the boundary of the thickening carries a positive measure w.r.t. a given Borel probability measure.

[RemyDegenne]

Is there a relation between closure (thickening δ E) and cthickening δ E you could add? There should be at least an inclusion, perhaps even equality?

[kkytola]

Is there a relation between closure (thickening δ E) and cthickening δ E you could add? There should be at least an inclusion, perhaps even equality?

Yes --- only the inclusion, though. I can add this inclusion, either in this PR or a follow-up. I will in any case be following up with more on thickenings (at least as much as is needed for the portmanteau theorem); I just wanted to split to manageable size PR chunks.

Is it better to add this in the present PR or a follow-up?

[RemyDegenne]

The inclusion can be kept for later if you want. Let's change the thickening_subset_cthickening lemma and merge this.

[kkytola]

Another thing that I should eventually add, but originally thought of including in a follow-up, is the cthickening versions of cthickening_eq_Inter_thickening and closure_eq_Inter_thickening, i.e., lemmas called cthickening_eq_Inter_cthickening and closure_eq_Inter_cthickening.

In this regard the order in my PRs was probably suboptimal, since the proof of cthickening_eq_Inter_cthickening should probably be given first (essentially the same as cthickening_eq_Inter_thickening in this PR) and then the open thickening case follows simply from it. In any case I would refactor, but one possibility is to change this PR very slightly to do the closed thickening case instead of the open thickening case. Or I could do both, by adding two more lemmas.

Again the main question is if more should be included in this PR, or should these be in follow-ups. I am trying to keep individual PRs small.

[Edit: After a bit of thinking, my preference is now to do an extremely minor change to replace the two last lemmas in this PR by their closed thickening counterparts. This should mean there is no need to touch them again in the follow-up. I did that now in 83d2dc1, hopefully ok?]

[RemyDegenne]

Thanks. let's wait for CI and merge.
bors d+

[bors]

✌️ kkytola can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kkytola]

Thank you!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests