ses2 sorry-free

Stream: condensed mathematics

[Kevin Buzzard]

Filippo and I have recently been working on the fiddly real analysis involved to prove lemma 2.5.14 of the blueprint. I've just finished the final sorry and pushed to master, which compiles, so if my understanding is correct then both the blue M-ses and theta.bounded ovals can now be turned green. For some reason the blueprint link to theta.bounded doesn't work for me, but the M-ses link does and links to a theorem in laurent_measures/ses2 . This file compiles on master with no complaints about sorries either in the file or in imports, so I think we must have done it; however I've also just noticed that the M-ses link links to a random commit rather than master, so you can still see sorries in github if you click on the blueprint link.

Also, the map we used to go from L_{r'}(S) to L_{r'}(S) is not multiplication by 2T-1 but by T^{-1} - 2, thus the blueprint is slightly incorrect. The latter map had better boundedness properties.

[Filippo A. E. Nuccio]

We are currently fixing the blueprint around that point, so you should not worry too much for now. I hope to upgrade that very soon.

[Johan Commelin]

A bit late, but see https://leanprover-community.github.io/liquid/dep_graph_section_2.html for the update if you haven't found that link yet.