Reverse Minkowski theorem

DefinitionGaussian mass of a lattice#✓fully proved

For a real number \(s\) and a \(\mathbb{Z}\)-submodule \(\mathcal{L} \subseteq \mathbb{R}^n\), the Gaussian mass of \(\mathcal{L}\) at parameter \(s\) is \(\rho_s(\mathcal{L}) = \sum_{y \in \mathcal{L}} e^{-\pi \|y\|^2 / s^2}\), where \(\|y\|\) is the Euclidean norm.

The sum is taken to be \(0\) when the series is not summable.

noncomputable def ρ (s : ℝ) (ℒ : Submodule ℤ ℝⁿ) : ℝ := ∑' y : ℒ, rexp (- π * ‖y‖ ^ 2 / s ^ 2)

Used by 1

Used byReverse Minkowski theorem

DefinitionBasis matrix of a lattice#✓fully proved

Let \(\mathcal{L} \subseteq \mathbb{R}^n\) be a discrete \(\mathbb{Z}\)-submodule of rank \(m\). Its basis matrix \(B(\mathcal{L})\) is the real \(n \times m\) matrix whose \(j\)-th column is the \(j\)-th vector of a fixed, arbitrarily chosen \(\mathbb{Z}\)-basis of \(\mathcal{L}\).

noncomputable def B (ℒ : Submodule ℤ ℝⁿ) [DiscreteTopology ℒ] :
    Matrix (Fin n) (Fin (finrank ℤ ℒ)) ℝ := (of fun i ↦ (finBasis ℤ ℒ) i).transpose

Used by 1

Used byDeterminant of a lattice

DefinitionDeterminant of a lattice#✓fully proved

For a discrete \(\mathbb{Z}\)-submodule \(\mathcal{L} \subseteq \mathbb{R}^n\) with basis matrix \(B = B(\mathcal{L})\) (the real matrix whose columns form a fixed \(\mathbb{Z}\)-basis of \(\mathcal{L}\)), the determinant of \(\mathcal{L}\) is \(\det(\mathcal{L}) = \sqrt{\det(B^{T} B)}\).

noncomputable def determinant (ℒ : Submodule ℤ ℝⁿ) [DiscreteTopology ℒ] : ℝ :=
  √ ((B ℒ).transpose * B ℒ).det

Uses 1 · Used by 1

Statement usesBasis matrix of a lattice

Used byReverse Minkowski theorem

TheoremReverse Minkowski theorem#●ready to prove

Let \(\mathcal{L} \subseteq \mathbb{R}^n\) be a full-rank lattice, that is, a discrete subgroup of \(\mathbb{R}^n\) that spans \(\mathbb{R}^n\), such that every subgroup \(\mathcal{L}' \subseteq \mathcal{L}\) (a lattice of possibly lower rank) has determinant \(\det(\mathcal{L}') \ge 1\). Let \(t = 10(\log n + 2)\), where \(\log\) is the natural logarithm. Then the Gaussian mass of \(\mathcal{L}\) at parameter \(1/t\) satisfies \(\rho_{1/t}(\mathcal{L}) = \sum_{y \in \mathcal{L}} e^{-\pi t^2 \|y\|^2} \le 3/2\), where \(\|y\|\) is the Euclidean norm.

public theorem_wanted theorem_1_2 (ℒ : Submodule ℤ ℝⁿ) [DiscreteTopology ℒ] (hℒ : IsZLattice ℝ ℒ)
    (h : ∀ ℒ' (_hℒℒ' : ℒ' ≤ ℒ) [DiscreteTopology ℒ'], determinant ℒ' ≥ 1) :
    let t : ℝ := 10 * (log n + 2)
    ρ (1 / t) ℒ ≤ 3 / 2

Sources

• O. Regev, N. Stephens-Davidowitz, A reverse Minkowski theorem, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_reverse_minkowski of the lean-eval benchmark.

Uses 2

Statement usesDeterminant of a lattice · Gaussian mass of a lattice

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.