Documentation

TauCeti.LinearAlgebra.IntegralLattice.PosDef.Minimum

The minimum and the kissing number of a positive definite lattice #

The minimum of a positive definite integral lattice L of positive rank is the least norm of a nonzero lattice vector,

min L = min {B(x, x) | x ∈ L, x ≠ 0},

a positive integer, and the kissing number is the number of nonzero vectors attaining it, that is the representation number r_L(min L).

Both are defined for every integral lattice, as natural numbers: the minimum is the least natural number that is the norm of a nonzero lattice vector, and it is 0 when there is none, which for a positive definite lattice happens exactly in rank zero; the kissing number is the cardinality of the set of nonzero vectors of norm min L, so that it is 0 in rank zero. For a positive definite lattice that set is finite and the kissing number is a genuine count; for a lattice whose minimal shell is infinite it is 0, as for representationNumber. The attainment and order properties of the minimum need only that norms are nonnegative, and are stated for positive semidefinite lattices: the minimum of a nontrivial positive semidefinite lattice is attained and bounds every nonzero norm from below, so it is the least element of the set of norms of nonzero vectors, which is the form in which a stored minimum is certified. Positive definiteness enters where it is needed: the minimum of a nontrivial positive definite lattice is positive, and its kissing number is a positive count of a finite shell.

An even positive definite lattice has minimum at least 2, and its minimum is exactly 2 as soon as it has a root, a vector of norm 2. Minimum and kissing number are isometry invariants.

Main declarations #

References #

source
noncomputable def TauCeti.IntegralLattice.minimum {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
ℕ

The minimum min L of an integral lattice: the least natural number that is the integral norm of a nonzero lattice vector, and 0 if there is none. For a positive definite lattice of positive rank this is the least norm of a nonzero vector, and it is positive.

Equations
Instances For
    source
    theorem TauCeti.IntegralLattice.minimum_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.minimum = sInf {k : ℕ | ∃ (x : ↥L.carrier), x ≠ 0 ∧ L.integralNorm x = ↑k}

    The minimum is the infimum of the natural numbers that are norms of nonzero lattice vectors.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.minimum_eq_zero_of_subsingleton {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [Subsingleton ↥L.carrier] :
    L.minimum = 0

    In rank zero there is no nonzero vector, so the minimum is 0.

    Positive semidefinite lattices #

    source
    theorem TauCeti.IntegralLattice.IsPosSemidef.exists_ne_zero_integralNorm_eq_minimum {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) [Nontrivial ↥L.carrier] :
    ∃ (x : ↥L.carrier), x ≠ 0 ∧ L.integralNorm x = ↑L.minimum

    In a nontrivial positive semidefinite lattice the minimum is the norm of some nonzero vector.

    source
    theorem TauCeti.IntegralLattice.IsPosSemidef.minimum_le_integralNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) {x : ↥L.carrier} (hx : x ≠ 0) :
    ↑L.minimum ≤ L.integralNorm x

    In a positive semidefinite lattice the minimum bounds the norm of every nonzero vector from below.

    source
    theorem TauCeti.IntegralLattice.IsPosSemidef.isLeast_minimum {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) [Nontrivial ↥L.carrier] :
    IsLeast {k : ℤ | ∃ (x : ↥L.carrier), x ≠ 0 ∧ L.integralNorm x = k} ↑L.minimum

    The minimum of a nontrivial positive semidefinite lattice is the least norm of a nonzero vector.

    source
    theorem TauCeti.IntegralLattice.IsPosSemidef.nonempty_vectorsOfNorm_minimum {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) [Nontrivial ↥L.carrier] :
    (L.vectorsOfNorm ↑L.minimum).Nonempty

    In a nontrivial positive semidefinite lattice the shell of the minimum is nonempty.

    source
    theorem TauCeti.IntegralLattice.IsPosSemidef.vectorsOfNorm_eq_empty_of_lt_minimum {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) {n : ℚ} (hn₀ : n ≠ 0) (hn : n < ↑L.minimum) :
    L.vectorsOfNorm n = ∅

    A positive semidefinite lattice represents no nonzero number below its minimum.

    Positive definite lattices #

    source
    theorem TauCeti.IntegralLattice.IsPosDef.minimum_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) [Nontrivial ↥L.carrier] :
    0 < L.minimum

    The minimum of a nontrivial positive definite lattice is positive.

    source
    theorem TauCeti.IntegralLattice.IsPosDef.minimum_eq_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) :
    L.minimum = 0 ↔ Subsingleton ↥L.carrier

    The minimum of a positive definite lattice vanishes exactly when the lattice has rank zero.

    Even lattices #

    source
    theorem TauCeti.IntegralLattice.IsPosDef.two_le_minimum {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (he : L.IsEven) [Nontrivial ↥L.carrier] :
    2 ≤ L.minimum

    The minimum of a nontrivial even positive definite lattice is at least 2.

    source
    theorem TauCeti.IntegralLattice.IsPosDef.minimum_eq_two {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (he : L.IsEven) {x : ↥L.carrier} (hx : L.integralNorm x = 2) :
    L.minimum = 2

    An even positive definite lattice with a root has minimum 2. A root is a lattice vector of norm 2.

    The kissing number #

    source
    noncomputable def TauCeti.IntegralLattice.kissingNumber {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    ℕ

    The kissing number of an integral lattice: the number of nonzero vectors of norm min L. For a positive definite lattice the minimal shell is finite, so this is a genuine count; on an infinite minimal shell it is 0. When the minimum is nonzero, in particular for a positive definite lattice of positive rank, this is the representation number r_L(min L) (kissingNumber_eq_representationNumber); in rank zero it is 0 (kissingNumber_eq_zero_of_subsingleton), the zero vector not being a minimal vector.

    Equations
    Instances For
      source
      theorem TauCeti.IntegralLattice.kissingNumber_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
      L.kissingNumber = (L.vectorsOfNorm ↑L.minimum \ {0}).ncard

      The kissing number is the cardinality of the set of nonzero vectors in the shell of the minimum, which is 0 when that set is infinite.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.kissingNumber_eq_zero_of_subsingleton {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [Subsingleton ↥L.carrier] :
      L.kissingNumber = 0

      In rank zero there is no nonzero vector, so the kissing number is 0.

      source
      theorem TauCeti.IntegralLattice.kissingNumber_eq_representationNumber {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (h : L.minimum ≠ 0) :
      L.kissingNumber = L.representationNumber ↑L.minimum

      When the minimum is nonzero, the kissing number is the representation number of the minimum.

      source
      theorem TauCeti.IntegralLattice.IsPosDef.kissingNumber_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) [Nontrivial ↥L.carrier] :
      0 < L.kissingNumber

      A nontrivial positive definite lattice has a positive kissing number.

      Isometry invariance #

      source
      theorem TauCeti.IntegralLattice.Isometry.minimum_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
      L.minimum = M.minimum

      The minimum is an isometry invariant.

      source
      theorem TauCeti.IntegralLattice.Isometry.kissingNumber_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
      L.kissingNumber = M.kissingNumber

      The kissing number is an isometry invariant.