Displaying similar documents to “The geometry of badly approximable vectors.”

Dual Lattice of ℤ-module Lattice

Yuichi Futa, Yasunari Shidama (2017)

Formalized Mathematics

Similarity:

In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic...

Embedded Lattice and Properties of Gram Matrix

Yuichi Futa, Yasunari Shidama (2017)

Formalized Mathematics

Similarity:

In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].