OAI/Combinatorics/Progressions/Lattices/StandardLatticeCoordinates.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.projectedIntegerLattice line 16
  2. def OAI.Erdos3.projectedIntegerGenerator line 19
  3. theorem OAI.Erdos3.projectedIntegerGenerator_mem line 22
  4. theorem OAI.Erdos3.projectedIntegerGenerator_norm_le line 27
  5. theorem OAI.Erdos3.projectedIntegerGenerator_span line 32
  6. theorem OAI.Erdos3.projectedIntegerGenerator_integer_span line 43
  7. theorem OAI.Erdos3.standardLatticeSection_full_of_integral_span line 49
  8. instance OAI.Erdos3.projectedIntegerLattice_discrete line 60
  9. instance OAI.Erdos3.projectedIntegerLattice_full line 73
  10. theorem OAI.Erdos3.standardEuclideanLattice_covolume line 90
  11. theorem OAI.Erdos3.projectedIntegerLattice_covolume line 102
  12. def OAI.Erdos3.rationalKernelAxisBound line 134
  13. theorem OAI.Erdos3.projectedIntegerLattice_norm_inv_le_of_rational_kernel line 137
  14. theorem OAI.Erdos3.basisAxisScale_le_of_rational_kernel line 194
  15. theorem OAI.Erdos3.exists_bounded_integral_span_of_rational_range line 219
  16. theorem OAI.Erdos3.rationalRangeLattice_full line 279
  17. theorem OAI.Erdos3.jointRationalSpaceLattice_full line 293
  18. theorem OAI.Erdos3.exists_short_projected_integer_basis line 314
  19. def OAI.Erdos3.standardLatticeIntegerLift line 341
  20. theorem OAI.Erdos3.standardLatticeIntegerLift_projection line 347
  21. def OAI.Erdos3.standardLatticeCoordinates line 355
  22. theorem OAI.Erdos3.standardLatticeCoordinates_reconstruction line 364
  23. theorem OAI.Erdos3.standardLatticeCoordinates_projection line 375
  24. theorem OAI.Erdos3.standardLatticeCoordinates_residue line 387