OAI/Combinatorics/Progressions/Nilpotent/AllocatedNiltestSourceSelection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_nested_box_niltest_detection line 18
  2. theorem OAI.Erdos3.exists_finite_site_niltest_detection line 65
  3. theorem OAI.Erdos3.exists_sampled_niltest_cube_detection line 104
  4. theorem OAI.Erdos3.exists_sampled_niltest_cube_detection_with_sides line 175
  5. theorem OAI.Erdos3.exists_sampled_niltest_fullbox_detection line 248
  6. theorem OAI.Erdos3.exists_sampled_niltest_fullbox_detection_uniform line 324
  7. def OAI.Erdos3.sampledSlicedDetectionConstant line 370
  8. theorem OAI.Erdos3.sampledSlicedDetectionConstant_two_le line 373
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_niltest_sliced_detection line 423
  10. def OAI.Erdos3.sampledFullboxDetectionConstant line 494
  11. theorem OAI.Erdos3.sampledFullboxDetectionConstant_two_le line 497
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_niltest_selection line 547