OAI/Combinatorics/Progressions/Lattices/RectangularLatticeCells.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.latticeSample line 15
  2. def OAI.Erdos3.latticeSamplingCell line 17
  3. theorem OAI.Erdos3.latticeSamplingCell_measurable line 20
  4. theorem OAI.Erdos3.latticeSamplingCell_iff line 23
  5. theorem OAI.Erdos3.latticeSamplingCell_volume line 30
  6. theorem OAI.Erdos3.latticeSample_error line 36
  7. theorem OAI.Erdos3.latticeSample_measurable line 49
  8. def OAI.Erdos3.finiteLatticeHistogram line 64
  9. theorem OAI.Erdos3.latticeSamplingCell_indicator_integrable line 67
  10. theorem OAI.Erdos3.finiteLatticeHistogram_integrable line 72
  11. theorem OAI.Erdos3.finiteLatticeHistogram_integral line 78
  12. theorem OAI.Erdos3.finiteLatticeHistogram_eq_floor line 90
  13. def OAI.Erdos3.rectangularLatticePoint line 118
  14. def OAI.Erdos3.rectangularLatticeRound line 121
  15. def OAI.Erdos3.rectangularLatticeSample line 124
  16. def OAI.Erdos3.rectangularLatticeCell line 127
  17. theorem OAI.Erdos3.rectangularLatticeCell_measurable line 130
  18. theorem OAI.Erdos3.rectangularLatticeCell_iff line 135
  19. theorem OAI.Erdos3.rectangularLatticeCell_volume line 141
  20. theorem OAI.Erdos3.rectangularLatticeCell_volume_ne_top line 147
  21. theorem OAI.Erdos3.rectangularLatticeSample_error line 154
  22. theorem OAI.Erdos3.rectangularLatticeSample_measurable line 162