OAI/Combinatorics/Progressions/Lattices/ResidueSliceNormalizedCell.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.ResidueBoxSlice line 12
  2. def OAI.Erdos3.ResidueBoxSlice.point line 21
  3. def OAI.Erdos3.ResidueBoxSlice.center line 24
  4. theorem OAI.Erdos3.ResidueBoxSlice.point_residue line 27
  5. abbrev OAI.Erdos3.ResidueBoxSlice.ofBlocks line 31
  6. theorem OAI.Erdos3.ResidueBoxSlice.ofBlocks_point line 38
  7. theorem OAI.Erdos3.FiniteProgressionPartition.entireResidue_length_ge line 58
  8. def OAI.Erdos3.FiniteProgressionPartition.comparableResidues line 80
  9. theorem OAI.Erdos3.FiniteProgressionPartition.comparableResidues_step line 85
  10. theorem OAI.Erdos3.FiniteProgressionPartition.comparableResidues_length line 91
  11. theorem OAI.Erdos3.exists_partition_cell_average line 101
  12. theorem OAI.Erdos3.exists_comparable_residueBoxSlice line 128
  13. theorem OAI.Erdos3.exists_narrow_residueBoxSlice line 156
  14. theorem OAI.Erdos3.denseResidueMeshInterval line 200
  15. theorem OAI.Erdos3.denseResidueMeshInterval_code_bound line 222
  16. theorem OAI.Erdos3.ResidueBoxSlice.residueIndex_endpoint_le line 233
  17. def OAI.Erdos3.ResidueBoxSlice.meshRounded line 241
  18. theorem OAI.Erdos3.ResidueBoxSlice.meshRounded_length_pos line 258
  19. theorem OAI.Erdos3.ResidueBoxSlice.meshRounded_contained line 266
  20. theorem OAI.Erdos3.ResidueBoxSlice.log_side_loss line 304
  21. theorem OAI.Erdos3.ResidueBoxSlice.log_volume_loss line 312
  22. theorem OAI.Erdos3.ResidueBoxSlice.spatial_freezing_log_side_loss line 319
  23. def OAI.Erdos3.ResidueBoxSlice.parameters line 343
  24. theorem OAI.Erdos3.ResidueBoxSlice.parameters_degree line 346
  25. def OAI.Erdos3.ResidueBoxSlice.reparamPatch line 351
  26. theorem OAI.Erdos3.ResidueBoxSlice.reparamPatch_kernel line 354
  27. theorem OAI.Erdos3.ResidueBoxSlice.reparamPatch_value line 357
  28. theorem OAI.Erdos3.exists_normalized_cell_of_coordinate_intervals line 374
  29. theorem OAI.Erdos3.ResidueBoxSlice.exists_affine_normalized_cell line 405