OAI/Combinatorics/Progressions/Lattices/EuclideanShortLatticeBasis.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.orthonormalChart line 17
  2. theorem OAI.Erdos3.orthonormalChart_norm_le line 21
  3. theorem OAI.Erdos3.orthonormalChart_symm_norm_le line 34
  4. def OAI.Erdos3.orthonormalCoordinateLattice line 41
  5. instance OAI.Erdos3.orthonormalCoordinateLattice_discrete line 45
  6. instance OAI.Erdos3.orthonormalCoordinateLattice_full line 49
  7. theorem OAI.Erdos3.orthonormalChart_measurePreserving line 56
  8. theorem OAI.Erdos3.orthonormalCoordinateLattice_covolume line 60
  9. theorem OAI.Erdos3.exists_short_euclidean_lattice_basis line 76