OAI/Combinatorics/Progressions/Fourier/ExponentialBohrVolume.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.CyclicBohr.character line 19
  2. lemma OAI.Erdos3.CyclicBohr.character_zero line 22
  3. lemma OAI.Erdos3.CyclicBohr.character_add line 25
  4. lemma OAI.Erdos3.CyclicBohr.norm_character line 29
  5. lemma OAI.Erdos3.CyclicBohr.character_comm line 32
  6. lemma OAI.Erdos3.CyclicBohr.character_zero_index line 42
  7. lemma OAI.Erdos3.CyclicBohr.character_add_index line 45
  8. lemma OAI.Erdos3.CyclicBohr.norm_one_sub_mul_of_norm_le_one line 49
  9. structure OAI.Erdos3.CyclicBohr.Set line 58
  10. def OAI.Erdos3.CyclicBohr.Set.carrier line 65
  11. instance OAI.Erdos3.CyclicBohr.Set.(instance at line 69) line 69
  12. lemma OAI.Erdos3.CyclicBohr.Set.mem_carrier line 71
  13. lemma OAI.Erdos3.CyclicBohr.Set.mem_iff line 76
  14. def OAI.Erdos3.CyclicBohr.Set.rank line 80
  15. def OAI.Erdos3.CyclicBohr.Set.dilate line 82
  16. def OAI.Erdos3.CyclicBohr.Set.ofFrequencies line 87
  17. def OAI.Erdos3.CyclicBohr.Set.meet line 92
  18. lemma OAI.Erdos3.CyclicBohr.Set.frequencies_ofFrequencies line 97
  19. lemma OAI.Erdos3.CyclicBohr.Set.radius_ofFrequencies line 100
  20. lemma OAI.Erdos3.CyclicBohr.Set.rank_ofFrequencies line 103
  21. lemma OAI.Erdos3.CyclicBohr.Set.frequencies_meet line 106
  22. lemma OAI.Erdos3.CyclicBohr.Set.radius_meet line 109
  23. lemma OAI.Erdos3.CyclicBohr.Set.rank_meet_le line 112
  24. lemma OAI.Erdos3.CyclicBohr.Set.frequencies_dilate line 115
  25. lemma OAI.Erdos3.CyclicBohr.Set.radius_dilate line 118
  26. lemma OAI.Erdos3.CyclicBohr.Set.rank_dilate line 121
  27. lemma OAI.Erdos3.CyclicBohr.Set.zero_mem line 124
  28. lemma OAI.Erdos3.CyclicBohr.Set.carrier_nonempty line 129
  29. lemma OAI.Erdos3.CyclicBohr.Set.card_pos line 132
  30. lemma OAI.Erdos3.CyclicBohr.Set.neg_mem_iff line 135
  31. lemma OAI.Erdos3.CyclicBohr.Set.add_mem_of_mem line 148
  32. lemma OAI.Erdos3.CyclicBohr.Set.add_mem_dilate line 163
  33. lemma OAI.Erdos3.CyclicBohr.Set.sub_mem_dilate line 174
  34. lemma OAI.Erdos3.CyclicBohr.Set.carrier_mono line 181
  35. lemma OAI.Erdos3.CyclicBohr.Set.carrier_meet_subset_left line 188
  36. lemma OAI.Erdos3.CyclicBohr.Set.carrier_meet_subset_right line 193
  37. lemma OAI.Erdos3.CyclicBohr.Set.dilate_mono line 198
  38. lemma OAI.Erdos3.CyclicBohr.Set.carrier_eq_univ_of_two_le_radius line 207
  39. lemma OAI.Erdos3.CyclicBohr.Set.dilate_one line 218
  40. lemma OAI.Erdos3.CyclicBohr.Set.dilate_dilate line 222
  41. lemma OAI.Erdos3.CyclicBohr.norm_sub_le_abs_arg_sub_of_norm_eq_one line 244
  42. def OAI.Erdos3.CyclicBohr.scaledArg line 275
  43. lemma OAI.Erdos3.CyclicBohr.scaledArg_nonneg line 278
  44. lemma OAI.Erdos3.CyclicBohr.scaledArg_le line 283
  45. def OAI.Erdos3.CyclicBohr.argBin line 291
  46. lemma OAI.Erdos3.CyclicBohr.abs_scaledArg_sub_lt_one_of_argBin_eq line 296
  47. lemma OAI.Erdos3.CyclicBohr.abs_arg_sub_lt_of_argBin_eq line 314
  48. def OAI.Erdos3.CyclicBohr.argumentCode line 332
  49. lemma OAI.Erdos3.CyclicBohr.card_argumentCodeSpace line 336
  50. lemma OAI.Erdos3.CyclicBohr.norm_one_sub_character_sub line 341
  51. lemma OAI.Erdos3.CyclicBohr.sub_mem_of_argumentCode_eq line 348
  52. theorem OAI.Erdos3.CyclicBohr.natDiv_codeCard_le_card_carrier line 364
  53. lemma OAI.Erdos3.CyclicBohr.abs_arg_character_le_two_radius line 401
  54. def OAI.Erdos3.CyclicBohr.localScaledArg line 420
  55. lemma OAI.Erdos3.CyclicBohr.localScaledArg_nonneg line 423
  56. lemma OAI.Erdos3.CyclicBohr.localScaledArg_le_eight line 432
  57. def OAI.Erdos3.CyclicBohr.localArgBin line 441
  58. def OAI.Erdos3.CyclicBohr.localArgumentCode line 447
  59. lemma OAI.Erdos3.CyclicBohr.card_localArgumentCodeSpace line 451
  60. lemma OAI.Erdos3.CyclicBohr.abs_localScaledArg_sub_lt_one_of_localArgBin_eq line 455
  61. lemma OAI.Erdos3.CyclicBohr.abs_arg_sub_lt_half_radius_of_localArgBin_eq line 484
  62. lemma OAI.Erdos3.CyclicBohr.sub_mem_half_dilate_of_localArgumentCode_eq line 507
  63. theorem OAI.Erdos3.CyclicBohr.card_carrier_le_nine_pow_rank_mul_card_half line 527
  64. lemma OAI.Erdos3.CyclicBohr.Set.norm_one_sub_prod_le_sum line 583
  65. lemma OAI.Erdos3.CyclicBohr.Set.character_sum line 594
  66. lemma OAI.Erdos3.CyclicBohr.Set.character_neg_index line 602
  67. lemma OAI.Erdos3.CyclicBohr.Set.norm_one_sub_character_neg_index line 607
  68. def OAI.Erdos3.CyclicBohr.Set.signedSpan line 612
  69. lemma OAI.Erdos3.CyclicBohr.Set.norm_one_sub_character_le_rank_mul line 615
  70. lemma OAI.Erdos3.CyclicBohr.character_eq_one_mul line 645
  71. lemma OAI.Erdos3.CyclicBohr.norm_one_sub_character_intCast line 650
  72. lemma OAI.Erdos3.CyclicBohr.norm_one_sub_character_le_of_mul_eq_intCast line 668
  73. theorem OAI.Erdos3.CyclicBohr.card_le_codeCard_mul_card line 687
  74. theorem OAI.Erdos3.CyclicBohr.card_lower_bound line 711
  75. theorem OAI.Erdos3.CyclicBohr.card_two_le_nine_pow_three_rank_mul_card_quarter line 746
  76. theorem OAI.Erdos3.CyclicBohr.card_le_dyadic_dilate line 775
  77. theorem OAI.Erdos3.CyclicBohr.relative_card_lower_bound line 793
  78. theorem OAI.Erdos3.CyclicBohr.Set.card_lower_bound_of_quartic_rank line 837