OAI/Combinatorics/Progressions/Lattices/AffineMeshRetention.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.interval_event_probability line 15
  2. theorem OAI.Erdos3.interval_near_probability line 26
  3. theorem OAI.Erdos3.integer_box_near_probability line 45
  4. theorem OAI.Erdos3.integer_box_pair_near_probability line 59
  5. theorem OAI.Erdos3.integer_box_pair_near_probability_of_lengths line 70
  6. theorem OAI.Erdos3.integer_vector_content_natAbs_scale line 97
  7. theorem OAI.Erdos3.affine_parameter_difference_gcd line 104
  8. theorem OAI.Erdos3.integer_box_pair_gcd_probability line 113
  9. theorem OAI.Erdos3.affine_parameter_pair_gcd_probability line 134
  10. theorem OAI.Erdos3.integerBoxUniformWeights_mean line 162
  11. theorem OAI.Erdos3.finite_event_probability_or_le line 177
  12. def OAI.Erdos3.affineParameterBadPair line 186
  13. def OAI.Erdos3.integerBoxBadPairBudget line 192
  14. theorem OAI.Erdos3.affine_parameter_bad_pair_probability line 196
  15. theorem OAI.Erdos3.sampled_affine_integer_box_error line 212
  16. theorem OAI.Erdos3.expect_le_of_dependent_coordinate_slices line 244
  17. theorem OAI.Erdos3.integer_box_affine_near_probability line 263
  18. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceLaw_mean_eq_rectangle line 303
  19. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceRectangle_endpoint_bounds line 334
  20. theorem OAI.Erdos3.ResidueBoxSlice.fullSliceRectangle_endpoint_bounds_two line 361
  21. theorem OAI.Erdos3.integerBoxBadPairBudget_nonneg line 383
  22. theorem OAI.Erdos3.integerBoxBadPairBudget_le_separated line 388
  23. theorem OAI.Erdos3.integerBoxBadPairBudget_le_linear line 418
  24. theorem OAI.Erdos3.integerBox_weighted_joint_mean line 450
  25. theorem OAI.Erdos3.integerBox_joint_error_of_window_tests line 468
  26. def OAI.Erdos3.physicalBoundaryBudget line 501
  27. theorem OAI.Erdos3.integer_box_physical_boundary_probability line 505
  28. theorem OAI.Erdos3.sampled_physical_boundary_probability line 543
  29. def OAI.Erdos3.physicalMeshCrossing line 567
  30. theorem OAI.Erdos3.retained_mesh_cell_constant line 572
  31. theorem OAI.Erdos3.physicalMeshCrossing_congr line 581
  32. theorem OAI.Erdos3.physicalMeshCrossing_subset_boundary line 593
  33. theorem OAI.Erdos3.affine_mesh_crossing_probability line 604