Integral Lattice

Results named in Tau Ceti's TauCeti.LinearAlgebra.IntegralLattice modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremMilgram's theorem #

The Gauss-sum invariant of the discriminant form of an even nondegenerate lattice is its signature t₊ - t₋ modulo 8.

TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_eq_sigPos_sub_sigNeg.{u} {V : Type u}
  [AddCommGroup V] [_root_.Module ℚ V] (L : TauCeti.IntegralLattice V) [L.IsNondegenerate]
  (hL : L.IsEven) : (L.discriminantQuadraticModule hL).gaussSign = ↑L.sigPos - ↑L.sigNeg

Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_eq_sigPos_sub_sigNeg.

Other forms

Milgram's theorem for ⟨2m⟩. Formalized in Tau Ceti as TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_rankOne.

TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_rankOne (m : ℤ) [NeZero m] :
  ((TauCeti.IntegralLattice.rankOne (2 * m)).discriminantQuadraticModule ⋯).gaussSign = ↑m.sign

Sources

LeanTauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_eq_sigPos_sub_sigNeg · TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_rankOne

Uses 4

Statement usesTauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice · TauCeti.IntegralLattice.discriminantQuadraticModule

Proof usesEuler's four-square identity for a quadratic map

TheoremMinkowski's bound for the minimum #

A positive definite integral lattice of rank n satisfies min L ≤ (4 / π) · Γ(n/2 + 1) ^ (2/n) · (det L) ^ (1/n).

TauCeti.IntegralLattice.IsPosDef.minimum_le_mul_determinant_rpow.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef) :
  ↑L.minimum ≤
    4 / Real.pi *
        Real.Gamma (↑(Module.finrank ℤ ↥L.carrier) / 2 + 1) ^ (2 / ↑(Module.finrank ℤ ↥L.carrier)) *
      ↑L.determinant ^ (1 / ↑(Module.finrank ℤ ↥L.carrier))

Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.IsPosDef.minimum_le_mul_determinant_rpow.

Other forms

Minkowski's bound for the minimum, without roots. Formalized in Tau Ceti as TauCeti.IntegralLattice.IsPosDef.minimum_pow_mul_pi_pow_le.

TauCeti.IntegralLattice.IsPosDef.minimum_pow_mul_pi_pow_le.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef) :
  ↑L.minimum ^ Module.finrank ℤ ↥L.carrier * Real.pi ^ Module.finrank ℤ ↥L.carrier ≤
    4 ^ Module.finrank ℤ ↥L.carrier * Real.Gamma (↑(Module.finrank ℤ ↥L.carrier) / 2 + 1) ^ 2 *
      ↑L.determinant

Sources

LeanTauCeti.IntegralLattice.IsPosDef.minimum_le_mul_determinant_rpow · TauCeti.IntegralLattice.IsPosDef.minimum_pow_mul_pi_pow_le

Uses 2

Statement usesTauCeti.IntegralLattice

Proof usesMinkowski's second theorem

TheoremMinkowski's convex body theorem for a realized lattice #

Let φ realize a nondegenerate integral lattice L in a real inner product space E of dimension n. A convex set K ⊆ E, symmetric about the origin, of volume greater than 2ⁿ · √(det L) contains φ y for some nonzero y ∈ L.

TauCeti.IntegralLattice.exists_ne_zero_mem_of_two_pow_mul_sqrt_determinant_lt.{u, u_1} {V : Type u}
  [AddCommGroup V] [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [L.IsNondegenerate] {φ : ↥L.carrier →ₗ[ℤ] E}
  (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y))
  (hspan : Submodule.span ℝ (Set.range ⇑φ) = ⊤) {K : Set E} (hsymm : ∀ v ∈ K, -v ∈ K)
  (hconv : Convex ℝ K)
  (hK : ENNReal.ofReal (2 ^ Module.finrank ℝ E * √↑L.determinant) < MeasureTheory.volume K) :
  ∃ y, y ≠ 0 ∧ φ y ∈ K

Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.exists_ne_zero_mem_of_two_pow_mul_sqrt_determinant_lt.

Sources

LeanTauCeti.IntegralLattice.exists_ne_zero_mem_of_two_pow_mul_sqrt_determinant_lt

Uses 1 · Used by 1

Statement usesTauCeti.IntegralLattice

Used byMinkowski's second theorem

TheoremMinkowski's second theorem #

The successive minima λ₀, …, λ_{n-1} of a positive definite integral lattice of rank n satisfy (∏ᵢ λᵢ) · πⁿ ≤ 4ⁿ · Γ(n/2 + 1)² · det L, that is, ∏ᵢ λᵢ ≤ cₙⁿ · det L with cₙ = (4 / π) · Γ(n/2 + 1) ^ (2/n) the constant of Minkowski's bound for the minimum.

TauCeti.IntegralLattice.IsPosDef.prod_successiveMinimum_mul_pi_pow_le.{u} {V : Type u}
  [AddCommGroup V] [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef) :
  (∏ i, ↑(L.successiveMinimum i)) * Real.pi ^ Module.finrank ℤ ↥L.carrier ≤
    4 ^ Module.finrank ℤ ↥L.carrier * Real.Gamma (↑(Module.finrank ℤ ↥L.carrier) / 2 + 1) ^ 2 *
      ↑L.determinant