Minkowski Lattice Theorem

Stream: Is there code for X?

[Yaël Dillies]

Is anybody already working on Minkowski's theorem? https://en.wikipedia.org/wiki/Minkowski%27s_theorem
I'm thinking of formalising it.

[Johan Commelin]

I think @Alex J. Best has a PR on (parts of?) it

[Johan Commelin]

#2819

[Yaël Dillies]

Oh right, thanks! This seems a bit dead, though :frown:

[Alex J. Best]

@Yaël Dillies yes, it is quite dead! At the time I came to the conclusion that measure theory needed more development to prove some of the key results, https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/random.20PR.3A.20.5BWIP.5D.20feat.28number_theory.2Fgeometry_of_numbers.29.3A.2E.2E.2E/near/215254314 I think a lot of this is now possible thanks to the work of many people (lots of credit to Floris and Yury though!). So I definitely think its high time to revive this PR, or rewrite it completely lol. I think I will have more time for lean in the next few weeks (I just submitted my PhD thesis today!) so I'm happy to collaborate on this :smile:.

[Johan Commelin]

Congrats on submitting your thesis! :tada:

[Yaël Dillies]

I would love to collaborate with you on it! To put in context, I'm looking for a nice result (if possible in combinatorics) to formalize during my summer internship with Bhavik Mehta. How much time do you think still need to be poured in to make the proof work?

[Yaël Dillies]

Four years later, I am back at it: Now that Minkowski's theorem is in mathlib, I am considering formalising Minkowski's second theorem. Is anybody working on that?

[Yaël Dillies]

The statement is that, if $\Lambda$ is a lattice in $\R^d$ and $K \subseteq R^d$$ is a centrally symmetric convex body, then $\lambda_1 \dots \lambda_n \mathrm{vol}\ K \le \mathrm{covol}\ \Lambda$, where $\lambda_i$ is the $i$-th successive minimum of $K$, ie $\lambda_i := \inf\{\lambda ≥ 0 \mid \dim\mathrm{span}(\lambda K \cap \Lambda) \ge i\}$.

[Johan Commelin]

cc @Xavier Roblot ?

[Xavier Roblot]

No, I am not working on anything related to lattices at the moment. But I think it would be very interesting to have this result in Mathlib.

[Kevin Wilson]

Just noticed this thread…. @Yaël Dillies if you’re embarking on this, I would love to rely on it. The proof of Schmidt’s bounds I was hoping to formalize here rely on Minkowski’s second theorem: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Counting.20isomorphism.20classes/with/560866287

[Yaël Dillies]

Got it! The proof seems really quite advanced in comparison to the statement, so I might stop at defining the successive minima and proving the existence of a directional basis for now. I am trying to use this project as a way for my friend to learn lean.

[Kevin Wilson]

It is surprisingly tricky. In his book, Cassels says "The proof of [the upper bound in the second theorem] remains difficult," whereas the lower bound is "almost trivial."