OAI/Combinatorics/Progressions/Lattices/EuclideanDerivativeLattice.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coordinateScaleEquiv line 14
  2. theorem OAI.Erdos3.coordinateScaleEquiv_apply line 23
  3. theorem OAI.Erdos3.coordinateScaleEquiv_symm_apply line 26
  4. def OAI.Erdos3.derivativeShearEquiv line 29
  5. theorem OAI.Erdos3.derivativeShearEquiv_apply line 48
  6. def OAI.Erdos3.derivativeLatticeEquiv line 52
  7. theorem OAI.Erdos3.derivativeLatticeEquiv_apply line 63
  8. def OAI.Erdos3.standardProductBasis line 94
  9. theorem OAI.Erdos3.standardProductBasis_mem_iff line 98
  10. def OAI.Erdos3.derivativeLatticeBasis line 121
  11. def OAI.Erdos3.derivativeLattice line 124
  12. instance OAI.Erdos3.derivativeLattice_discrete line 127
  13. instance OAI.Erdos3.derivativeLattice_full line 131
  14. theorem OAI.Erdos3.derivativeLattice_mem_iff line 135
  15. theorem OAI.Erdos3.derivativeLattice_carrier line 152
  16. theorem OAI.Erdos3.derivativeGridPoint_shift_bound line 188
  17. theorem OAI.Erdos3.derivativeLattice_shortSpan_projection line 201
  18. def OAI.Erdos3.euclideanDerivativeLatticeBasis line 250
  19. def OAI.Erdos3.euclideanDerivativeLattice line 254
  20. instance OAI.Erdos3.euclideanDerivativeLattice_discrete line 257
  21. instance OAI.Erdos3.euclideanDerivativeLattice_full line 262
  22. theorem OAI.Erdos3.euclideanDerivativeLattice_mem_iff line 267
  23. theorem OAI.Erdos3.productEuclideanEquiv_mem_derivativeLattice line 281
  24. theorem OAI.Erdos3.exists_bounded_euclideanDerivativeLattice_family line 286