Schwarz–Milnor lemma

Stream: Is there code for X?

[Kkll]

Referring to https://en.wikipedia.org/wiki/%C5%A0varc%E2%80%93Milnor_lemma aka "The Fundamental Observation of Geometric Group Theory"

I think the pieces for this exist, but idk if there are plans for this lemma or GGT in general.

[Anand Rao Tadipatri]

Large parts of the Švarc–Milnor lemma appear to be formalised in the geometric-group-theory branch of mathlib, but this hasn't been PRed into main: https://github.com/leanprover-community/mathlib/blob/geometric-group-theory/src/group_theory/geometric/svarc_milnor.lean.

[Scott Morrison]

Note there's a long thread from last year https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Geometric.20group.20theory which may be helpful.

[Scott Morrison]

It seems @Georgi Kocharyan wrote the file that @Anand Rao linked to, and perhaps he could tell us if there are plans to PR this material to mathlib.

[Georgi Kocharyan]

Scott Morrison said:

It seems Georgi Kocharyan wrote the file that Anand Rao linked to, and perhaps he could tell us if there are plans to PR this material to mathlib.

This is a project I worked on a while ago and have kinda forgotten the details of, but I'd love to PR it to mathlib. It's pretty much done from my side so it would need a more experienced person to go over it and clean it up to make it PR-worthy (I've never PRed anything before so I doubt I've followed all the conventions perfectly, though I tried to as far as I could).
Happy to help with anything necessary to make this happen! Note that what I wrote relies on the marked_group framework written by Yaël Dillies, the details of which I'm not too familiar with.

[Yaël Dillies]

Marked group are in #18256. I've tried addressing the comment several times already, but for some reason my file is unworkable with in gitpod and leaves me in orange bar hell after a minute or two of editing whatever I do.

[Yaël Dillies]

To be clear on what's left to do, Schwarz-Milnor isn't yet sorry-free. Georgi did the "marking group API + quasi-isometry API -> SM" part. I did the "marking group API" part, except our works don't quite match up (yet). @Clara Löh did the "quasi-isometry API" part, except that it's optimised for teaching and not for mathlib (too many definitions, not enough lemmas, doesn't follow mathlib style). So what needs to be done is

• finish #18256, taking inspiration from branch#geometric-group-theory. This is what I currently can't do because orange bar hell.
• rework the quasi-isometry API into a mathlib-appropriate form and PR
• additionally, Georgi uses a function that's very similar to docs#metric.cthickening and which I think does the same thing in the cases of interest, so we should try to replace its uses by cthickening

[Yaël Dillies]

I agree with Georgi that all this is more of a Lean expert job (probably me, because I'm already familiar with the code, but if anyone else wants to take it up, please do) and is beyond his pay grade.