OAI/Combinatorics/Progressions/Estimates/PositiveCyclicCorrelation.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.intervalCutUpper line 11
  2. theorem OAI.Erdos3.intervalCutUpper_le_end line 14
  3. theorem OAI.Erdos3.intervalCutUpper_le_cut line 18
  4. theorem OAI.Erdos3.le_intervalCutUpper line 22
  5. theorem OAI.Erdos3.lt_intervalCutUpper line 30
  6. theorem OAI.Erdos3.exists_intervalCut line 38
  7. theorem OAI.Erdos3.intervalCut_unique line 56
  8. def OAI.Erdos3.cyclicCutCell line 67
  9. theorem OAI.Erdos3.mem_cyclicCutCell line 70
  10. theorem OAI.Erdos3.sum_cyclicCutCell_indicator line 75
  11. def OAI.Erdos3.cubeRepresentativeSum line 101
  12. theorem OAI.Erdos3.cubeRepresentativeSum_intCast line 104
  13. theorem OAI.Erdos3.cubeRepresentativeSum_zmodCast line 108
  14. theorem OAI.Erdos3.cubeRepresentativeSum_le line 112
  15. def OAI.Erdos3.cubeCarryShift line 119
  16. theorem OAI.Erdos3.exists_cube_carry_code line 122
  17. def OAI.Erdos3.commonCyclicCuts line 161
  18. theorem OAI.Erdos3.quarterLower_mem_commonCyclicCuts line 165
  19. theorem OAI.Erdos3.quarterUpper_mem_commonCyclicCuts line 170
  20. theorem OAI.Erdos3.wrap_mem_commonCyclicCuts line 175
  21. theorem OAI.Erdos3.zero_mem_commonCyclicCuts line 180
  22. theorem OAI.Erdos3.commonCyclicCuts_le line 184
  23. theorem OAI.Erdos3.commonCyclicCuts_card_le line 191
  24. theorem OAI.Erdos3.exists_mem_cyclicQuarter line 204
  25. theorem OAI.Erdos3.commonCyclicCut_short line 213
  26. theorem OAI.Erdos3.sum_commonCyclicCut_indicator line 231
  27. theorem OAI.Erdos3.commonCyclicCut_representative line 236
  28. theorem OAI.Erdos3.exists_correlating_commonCyclicCut line 264
  29. def OAI.Erdos3.translatedCyclicProduct line 301
  30. theorem OAI.Erdos3.translatedCyclicProduct_on_cut line 304
  31. theorem OAI.Erdos3.translatedCyclicProduct_norm_bound line 314
  32. theorem OAI.Erdos3.translatedCyclicProduct_cut_correlation line 323
  33. theorem OAI.Erdos3.exists_correlating_integer_product_interval line 342
  34. def OAI.Erdos3.integerCubeProductWithShift line 378
  35. theorem OAI.Erdos3.exists_cyclic_cube_product_interval line 382
  36. def OAI.Erdos3.doubleDifferenceCarryShift line 433
  37. def OAI.Erdos3.integerDoubleDifferenceWithShift line 436
  38. theorem OAI.Erdos3.exists_double_difference_carry_code line 440
  39. theorem OAI.Erdos3.exists_cyclic_double_difference_interval line 461
  40. theorem OAI.Erdos3.re_finiteCorrelation_mul_indicator line 515
  41. theorem OAI.Erdos3.retained_restricted_correlation_re line 522
  42. theorem OAI.Erdos3.exists_re_correlating_commonCyclicCut line 543
  43. theorem OAI.Erdos3.exists_re_correlating_integer_product_interval line 583