OAI/Combinatorics/Progressions/Estimates/PositiveShiftTestingGowers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.shift_detection_exponential_gap line 10
  2. def OAI.Erdos3.shiftDetectionLoss line 33
  3. theorem OAI.Erdos3.shiftDetectionLoss_nonneg line 36
  4. theorem OAI.Erdos3.shift_detection_exponential_product line 39
  5. def OAI.Erdos3.shiftDetectionPolynomial line 47
  6. theorem OAI.Erdos3.shiftDetectionPolynomial_eval line 51
  7. theorem OAI.Erdos3.exists_shiftDetectionLoss_fixed_power line 55
  8. def OAI.Erdos3.CyclicShiftTestingDetection line 72
  9. theorem OAI.Erdos3.cyclicShiftTestingDetection_of_product line 85
  10. theorem OAI.Erdos3.exists_cyclicShiftTestingDetection line 107
  11. theorem OAI.Erdos3.cyclic_translated_pair_niltest_detection line 130
  12. def OAI.Erdos3.CyclicTranslatedShiftTestingDetection line 181
  13. theorem OAI.Erdos3.cyclicTranslatedShiftTestingDetection_of_product line 195
  14. theorem OAI.Erdos3.exists_cyclicTranslatedShiftTestingDetection line 217
  15. theorem OAI.Erdos3.shiftTestingSeminorm_eq_zero_of_isEmpty line 242
  16. theorem OAI.Erdos3.PositiveShiftBasis.exists_testingFamily_gowers_detection line 254