OAI/Combinatorics/Progressions/Fourier/LocalBohrAlmostPeriodsRelative.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.CyclicBohr.Set.characterBasis line 16
  2. theorem OAI.Erdos3.CyclicBohr.Set.rank_characterBasis line 20
  3. theorem OAI.Erdos3.CyclicBohr.Set.radius_characterBasis line 24
  4. theorem OAI.Erdos3.CyclicBohr.Set.norm_one_sub_le_of_mem_characterBasis line 27
  5. theorem OAI.Erdos3.CyclicBohr.Set.norm_one_sub_le_of_mem_characterBasis_addSpan line 38
  6. def OAI.Erdos3.CyclicBohr.Set.adjoinCharacters line 62
  7. theorem OAI.Erdos3.CyclicBohr.Set.rank_adjoinCharacters_le line 66
  8. theorem OAI.Erdos3.CyclicBohr.Set.radius_adjoinCharacters line 72
  9. theorem OAI.Erdos3.CyclicBohr.Set.adjoinCharacters_subset_ndilate line 77
  10. theorem OAI.Erdos3.CyclicBohr.Set.norm_one_sub_le_of_relative_cover line 82
  11. theorem OAI.Erdos3.CyclicBohr.Set.exists_regular_bohr_of_relative_cover line 101
  12. theorem OAI.Erdos3.RelativeChangSanders.localChangBaseScale_pos line 142
  13. theorem OAI.Erdos3.RelativeChangSanders.exists_regular_relative_spectrum_controller line 147
  14. theorem OAI.Erdos3.finiteFourierCoeff_finiteIndicator line 218
  15. theorem OAI.Erdos3.finiteFourierCoeff_averagingKernel line 223
  16. theorem OAI.Erdos3.sum_sq_setFourierMultiplier line 236
  17. theorem OAI.Erdos3.fourierL1_triple_average_sq_le line 242
  18. theorem OAI.Erdos3.fourierL1_triple_average_le line 270
  19. theorem OAI.Erdos3.CyclicCrootSisask.finiteSetAverage_ofReal line 289
  20. theorem OAI.Erdos3.CyclicCrootSisask.iteratedFiniteSetAverage_ofReal line 297
  21. theorem OAI.Erdos3.CyclicCrootSisask.finiteIndicator_eq_ofReal_realSetIndicator line 307
  22. theorem OAI.Erdos3.CyclicCrootSisask.triple_average_ofReal line 313
  23. theorem OAI.Erdos3.CyclicCrootSisask.triple_translate_le_of_iterated_approx line 318
  24. theorem OAI.Erdos3.RelativeChangSanders.localChangBaseScale_le_one line 355
  25. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_bohr_triple_almostPeriods line 372
  26. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_bohr_triple_almostPeriods_relative line 446