OAI/Combinatorics/Progressions/Lattices/ConcreteAffineMeshBoundary.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerBoxMeshPoint line 13
  2. def OAI.Erdos3.integerBoxMesh line 22
  3. theorem OAI.Erdos3.integerBoxMesh_distance line 27
  4. theorem OAI.Erdos3.normalized_integerBoxMesh_distance line 44
  5. def OAI.Erdos3.integerBoxMeshPointEquiv line 69
  6. def OAI.Erdos3.integerBoxMeshCellEquiv line 78
  7. theorem OAI.Erdos3.integerBoxMeshCellEquiv_val line 92
  8. theorem OAI.Erdos3.integerBoxMesh_cell_mean line 99
  9. theorem OAI.Erdos3.integerBoxMesh_mean_partition line 115
  10. theorem OAI.Erdos3.integerWindow_cell_endpoints line 140
  11. theorem OAI.Erdos3.integerWindow_cell_endpoint_abs line 154
  12. theorem OAI.Erdos3.integerWindow_cell_half_scale line 168
  13. theorem OAI.Erdos3.affineIntegerInterval_endpoint_abs line 192
  14. theorem OAI.Erdos3.affineIntegerInterval_width_le line 206
  15. theorem OAI.Erdos3.exists_integerBox_width_bound line 217
  16. theorem OAI.Erdos3.integerBoxUniformWeights_eq_uniform line 242
  17. theorem OAI.Erdos3.integerBoxMesh_pair_cell_mean line 251
  18. theorem OAI.Erdos3.integerUnitResidue_expect_eq line 290
  19. theorem OAI.Erdos3.integerBox_partition_eventProbability_le line 302
  20. theorem OAI.Erdos3.integerBoxMesh_cell_realize line 345
  21. theorem OAI.Erdos3.retained_integer_mesh_boxes_classify line 363
  22. theorem OAI.Erdos3.affine_parameter_mesh_distance line 407
  23. theorem OAI.Erdos3.concrete_affine_mesh_boundary_probability line 428