OAI/Combinatorics/Progressions/Lattices/LatticeVoronoiPacking.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.latticeVoronoi line 19
  2. theorem OAI.Erdos3.latticeVoronoi_closed line 22
  3. theorem OAI.Erdos3.exists_sub_mem_latticeVoronoi line 27
  4. theorem OAI.Erdos3.latticeVoronoi_subset_closedBall line 39
  5. theorem OAI.Erdos3.latticeVoronoi_isAddFundamentalDomain line 46
  6. def OAI.Erdos3.shortVectorSpan line 90
  7. def OAI.Erdos3.shortVectorLattice line 93
  8. theorem OAI.Erdos3.mem_shortVectorSpan line 97
  9. theorem OAI.Erdos3.exists_shortVectorSpan_basis line 100
  10. instance OAI.Erdos3.shortVectorLattice_discrete line 107
  11. instance OAI.Erdos3.shortVectorLattice_full line 111
  12. theorem OAI.Erdos3.shortVectorLattice_covering line 122
  13. theorem OAI.Erdos3.lattice_points_mul_covolume_le_closedBall line 145
  14. theorem OAI.Erdos3.shortVectorLattice_covolume_packing line 177