OAI/Combinatorics/Progressions/Fourier/BohrTorusApproximation.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.CyclicBohr.Set.ndilate line 20
  2. theorem OAI.Erdos3.CyclicBohr.Set.radius_ndilate line 22
  3. theorem OAI.Erdos3.CyclicBohr.Set.rank_ndilate line 25
  4. theorem OAI.Erdos3.CyclicBohr.Set.ndilate_one line 28
  5. theorem OAI.Erdos3.CyclicBohr.Set.ndilate_ndilate line 30
  6. theorem OAI.Erdos3.CyclicBohr.Set.carrier_ndilate_mono line 33
  7. def OAI.Erdos3.CyclicBohr.Set.IsRankRegular line 37
  8. theorem OAI.Erdos3.CyclicBohr.Set.isRankRegular_ndilate_iff line 46
  9. theorem OAI.Erdos3.CyclicBohr.Set.log_card_growth_lt_five_mul_rank line 59
  10. def OAI.Erdos3.CyclicBohr.Set.normalizedLogCard line 104
  11. theorem OAI.Erdos3.CyclicBohr.Set.normalizedLogCard_monotone line 108
  12. theorem OAI.Erdos3.CyclicBohr.Set.normalizedLogCard_buffer_growth line 118
  13. theorem OAI.Erdos3.CyclicBohr.Set.exists_rankRegular_ndilate line 136
  14. def OAI.Erdos3.torusChordCutoff line 307
  15. theorem OAI.Erdos3.torusChordCutoff_range line 310
  16. theorem OAI.Erdos3.torus_character_map_lipschitz line 313
  17. theorem OAI.Erdos3.torusChordCutoff_lipschitz line 331
  18. def OAI.Erdos3.CyclicBohr.Set.approximationWidth line 348
  19. theorem OAI.Erdos3.CyclicBohr.Set.approximationWidth_pos line 351
  20. def OAI.Erdos3.CyclicBohr.Set.upperApprox line 354
  21. def OAI.Erdos3.CyclicBohr.Set.lowerApprox line 357
  22. theorem OAI.Erdos3.CyclicBohr.Set.upperApprox_range line 361
  23. theorem OAI.Erdos3.CyclicBohr.Set.lowerApprox_range line 364
  24. theorem OAI.Erdos3.CyclicBohr.Set.lowerApprox_le_upperApprox line 367
  25. theorem OAI.Erdos3.CyclicBohr.Set.upperApprox_eq_one line 371
  26. theorem OAI.Erdos3.CyclicBohr.Set.lowerApprox_eq_zero line 377
  27. theorem OAI.Erdos3.CyclicBohr.Set.lowerApprox_eq_one_inner line 387
  28. theorem OAI.Erdos3.CyclicBohr.Set.upperApprox_eq_zero_outer line 397
  29. theorem OAI.Erdos3.CyclicBohr.Set.approximation_sandwich line 408
  30. theorem OAI.Erdos3.CyclicBohr.Set.approximation_gap_le_shell line 418
  31. theorem OAI.Erdos3.CyclicBohr.Set.approximation_observables_lipschitz line 437
  32. theorem OAI.Erdos3.CyclicBohr.Set.add_mem_ndilate line 458
  33. theorem OAI.Erdos3.CyclicBohr.Set.sub_mem_ndilate line 463
  34. theorem OAI.Erdos3.CyclicBohr.Set.uniformMass_translation_le_shell line 468
  35. theorem OAI.Erdos3.CyclicBohr.Set.uniformMass_translation_le_of_rankRegular line 489
  36. theorem OAI.Erdos3.CyclicBohr.Set.exists_regular_dilate_with_translation_bound line 506
  37. theorem OAI.Erdos3.CyclicBohr.Set.sum_approximation_gap_le line 530
  38. theorem OAI.Erdos3.CyclicBohr.Set.mean_approximation_gap_le line 552
  39. theorem OAI.Erdos3.CyclicBohr.Set.mean_shifted_approximation_gap_le line 562
  40. theorem OAI.Erdos3.CyclicBohr.Set.mean_indicator_approximation_error_le line 575
  41. theorem OAI.Erdos3.LocalConvolution.square_mean_le_local_add_boundary line 609
  42. def OAI.Erdos3.CyclicBohr.Set.whole line 678
  43. theorem OAI.Erdos3.CyclicBohr.Set.rank_whole line 680
  44. theorem OAI.Erdos3.CyclicBohr.Set.radius_whole line 682
  45. theorem OAI.Erdos3.CyclicBohr.Set.carrier_whole line 684
  46. theorem OAI.Erdos3.CyclicBohr.Set.exists_controlled_regular_subdilate line 689
  47. theorem OAI.Erdos3.CyclicBohr.Set.average_sub_le_of_upperApprox line 734
  48. theorem OAI.Erdos3.CyclicBohr.Set.sum_average_sub_le_of_upperApprox line 759
  49. theorem OAI.Erdos3.CyclicBohr.Set.small_sum_average_of_upperApprox line 772
  50. theorem OAI.Erdos3.CyclicBohr.Set.carrier_eq_univ_of_rank_zero line 808
  51. theorem OAI.Erdos3.CyclicBohr.Set.carrier_ndilate_whole line 815
  52. theorem OAI.Erdos3.CyclicBohr.Set.isRankRegular_whole line 821
  53. theorem OAI.Erdos3.CyclicBohr.Set.exists_bounded_presentation line 828
  54. def OAI.Erdos3.CyclicBohr.Set.torusUpperApprox line 858
  55. def OAI.Erdos3.CyclicBohr.Set.torusLowerApprox line 862
  56. theorem OAI.Erdos3.CyclicBohr.Set.torus_approximation_ranges line 866
  57. theorem OAI.Erdos3.CyclicBohr.Set.torus_approximations_lipschitz line 871
  58. theorem OAI.Erdos3.CyclicBohr.Set.exists_torus_approximation_orbit line 880