OAI/Combinatorics/Progressions/Lattices/BoxResiduePartition.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerResidueCount line 15
  2. def OAI.Erdos3.rectangularResidueCount line 18
  3. def OAI.Erdos3.integerRectangleVolume line 21
  4. theorem OAI.Erdos3.rectangularResidueCount_eq_card line 24
  5. theorem OAI.Erdos3.rectangularResidueCount_relative_error line 31
  6. def OAI.Erdos3.integerIntervalEquivFin line 77
  7. theorem OAI.Erdos3.integerIntervalEquivFin_val line 91
  8. theorem OAI.Erdos3.integerIntervalEquivFin_symm_val line 97
  9. theorem OAI.Erdos3.rectangularResidueCount_pos line 110
  10. theorem OAI.Erdos3.rectangularResidueLaws_l1 line 123
  11. theorem OAI.Erdos3.exists_rectangular_residue_piece_discrepancy line 175
  12. def OAI.Erdos3.intervalCellLower line 208
  13. def OAI.Erdos3.intervalCellUpper line 211
  14. def OAI.Erdos3.intervalResidueCell line 214
  15. theorem OAI.Erdos3.intervalResidueCell_eq_iff line 218
  16. def OAI.Erdos3.intervalResidueCellEquiv line 240
  17. abbrev OAI.Erdos3.IntegerResidueBox line 274
  18. def OAI.Erdos3.boxIntervalResidueCell line 277
  19. def OAI.Erdos3.boxIntervalResidueCellEquiv line 282
  20. theorem OAI.Erdos3.boxIntervalResidueCell_card line 297
  21. theorem OAI.Erdos3.boxIntervalResidue_mixture line 311