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."

[Kevin Wilson]

Hi @Yaël Dillies I had a moment to get back to this, and I think that one approach would be to prove the theorem when the convex body is just the sphere. That's a much easier theorem (and pretty much just needs SVD and some accounting).

[Yaël Dillies]

Oh unfortunately that doesn't cover my use case, which would instead use a parallelepiped to show that a Bohr set contains a large generalised arithmetic progression.

[Kevin Wilson]

Hmm I don’t think it’s too much harder to prove in the case the convex body is the sphere of a norm. Is that true of your parallelepiped (eg if A is the basis of the parallelepiped then perhaps your parallelepiped is the sphere of x -> |A x|_oo?

[Kevin Wilson]

Hi @Yaël Dillies I took a shot at thinking through what the definition of successive minima should be. In basically every application I've come across, the convex body is just the ball of a norm. With that in mind, one definition of successive minimum that seems amenable to formalization is:

variable {E : Type*} [NormedAddCommGroup E] (L : Submodule ℤ E)

/-- The set of max-norms of linearly independent `(i+1)`-tuples from `L`. -/
def lambdaSet (i : ℕ) : Set ℝ :=
  (fun v ↦ ⨆ j, ‖(v j : E)‖) ''
    {v : Fin (i + 1) → L | LinearIndependent ℤ v}

/-- The `i`-th successive minimum of `L`. -/
noncomputable def successiveMinimum (i : ℕ) : ℝ := sInf (lambdaSet L i)

Then it's not hard to show (with some additional assumptions):

variable [NormedSpace ℝ E] [FiniteDimensional ℝ E] [hL : DiscreteTopology L]

theorem lambdaSet_finite_Iic (i : ℕ) (R : ℝ) : (lambdaSet L i ∩ Set.Iic R).Finite := sorry

theorem successiveMinimum_attained {i : ℕ} (hne : (lambdaSet L i).Nonempty) :
    ∃ v : Fin (i + 1) → L, LinearIndependent ℤ v ∧ ⨆ j, ‖(v j : E)‖ = successiveMinimum L i := sorry

It's a bit harder to show, but not too bad, so show

theorem successiveMinimum_set {i : ℕ} (hne : (lambdaSet L i).Nonempty) :
    ∃ v : Fin (i + 1) → L, LinearIndependent ℤ v ∧
      ∀ j : Fin (i + 1), ‖(v j : E)‖ = successiveMinimum L j := sorry

If you're OK with it, I'm happy to write that up!

[Yaël Dillies]

But then why not do it for any convex symmetric set? They all are the convex unit ball of some (semi)norm, namely their gauge: docs#gauge

[Yaël Dillies]

Btw I have some partial progress myself. Here it is: https://github.com/leanprover-community/mathlib4/compare/master...YaelDillies:successive_min

[Yaël Dillies]

I wanted to invite you to my fork so that you could push more stuff there, but I don't know your github handle! Please let me know once you have added it to your Zulip profile. Then I'll invite you

[Kevin Wilson]

Oh awesome! I’m @khwilson on GitHub

[Kevin Wilson]

An arbitary convex symmetric set includes, e.g., univ, and so some lemmas you’d expect to be true about successive minima (like they are positive) aren’t true for arbitrary convex symmetric sets.

So you can define it, but all the theorems I know assume something like “positive finite volume” or “bounded” which ends up implying the gauge is positive definite

[Kevin Wilson]

This is the version that I was working on, btw: https://gist.github.com/khwilson/8ccd681a4e1c46e92186cfb6020f9305

I like your approach to the directional set! Much cleaner than my reordering approach :-)

[Yaël Dillies]

Feel free to push stuff to my branch (and claim the copyright), I won't have time to work on this for the coming two months!

[Antoine Chambert-Loir]

What do you call the “second” Minkowski theorem on line 188? For me (and all the literature I ever read on the topic), it is the theorem on the product of successive minima, which is stronger than the theorem on the first minimum — that is sufficient to assert the existence of nontrivial lattice points.

[Antoine Chambert-Loir]

By the way, I feel useful that the definition of successive minima be not restricted to compact convex symmetric sets, but allow more flexibility. There are variants of the first Minkowski theorem in the non symmetric case, and the theory of indefinite forms is implicitly about non convex sets.

[Antoine Chambert-Loir]

While it is true that all compact convex symmetric sets come from (pseudo)norms, and norms are the relevant case for most practice, in mathlib, that would force the convex set to be given as an instance, and would probably make it complicated to play with several sets at once.

[Yaël Dillies]

Antoine Chambert-Loir said:

What do you call the “second” Minkowski theorem on line 188? For me (and all the literature I ever read on the topic), it is the theorem on the product of successive minima, which is stronger than the theorem on the first minimum — that is sufficient to assert the existence of nontrivial lattice points.

Is https://github.com/leanprover-community/mathlib4/compare/master...YaelDillies:successive_min#diff-d728076b79df3c449c6c40c677eca7d57697d5441e94647cd191a9abe59c3345R188-R194 not a theorem on the product of successive minima?

[Yaël Dillies]

Antoine Chambert-Loir said:

I feel useful that the definition of successive minima be not restricted to compact convex symmetric sets, but allow more flexibility. There are variants of the first Minkowski theorem in the non symmetric case, and the theory of indefinite forms is implicitly about non convex sets.

My version allows for this, a priori

[Antoine Chambert-Loir]

The theorem is about that, sorry, but the docstring doesn't seem to.

[Kevin Wilson]

OK, I got a chance to take a stab at this: https://github.com/leanprover-community/mathlib4/pull/35812

cc @Antoine Chambert-Loir @Yaël Dillies

The strategy ended up being a bit verbose (I took the sequential compactness approach, somewhat for my own edification). I also wasn't sure if there was a better place to move the filter inequalities. I searched the library for a bit, but no place seemed like a good home.

[Kevin Wilson]

(Also, sorry Yael, I didn't have permission to push to your branch, so I just copied your commit to my fork.)