OAI/Combinatorics/Progressions/Fourier/RectangularGridCharacter.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.CircleFourier.Circle line 19
  2. abbrev OAI.Erdos3.CircleFourier.circleHaar line 21
  3. theorem OAI.Erdos3.CircleFourier.circleHaar_eq_volume line 23
  4. def OAI.Erdos3.CircleFourier.integerDistance line 28
  5. theorem OAI.Erdos3.CircleFourier.integerDistance_nonneg line 30
  6. theorem OAI.Erdos3.CircleFourier.integerDistance_le_half line 32
  7. theorem OAI.Erdos3.CircleFourier.integerDistance_zero line 36
  8. theorem OAI.Erdos3.CircleFourier.integerDistance_neg line 40
  9. theorem OAI.Erdos3.CircleFourier.integerDistance_coe line 44
  10. def OAI.Erdos3.CircleFourier.character line 48
  11. theorem OAI.Erdos3.CircleFourier.character_zero line 51
  12. theorem OAI.Erdos3.CircleFourier.character_add line 55
  13. theorem OAI.Erdos3.CircleFourier.character_neg line 61
  14. theorem OAI.Erdos3.CircleFourier.character_nsmul line 68
  15. theorem OAI.Erdos3.CircleFourier.character_zsmul line 74
  16. theorem OAI.Erdos3.CircleFourier.character_finset_sum line 80
  17. theorem OAI.Erdos3.CircleFourier.character_fintype_sum line 88
  18. theorem OAI.Erdos3.CircleFourier.norm_character line 93
  19. theorem OAI.Erdos3.CircleFourier.character_eq_one_iff line 96
  20. def OAI.Erdos3.CircleFourier.geometricCharacterSum line 105
  21. theorem OAI.Erdos3.CircleFourier.geometricCharacterSum_mul line 108
  22. theorem OAI.Erdos3.CircleFourier.norm_character_sub_one_le_two line 113
  23. theorem OAI.Erdos3.CircleFourier.four_mul_integerDistance_le_norm_character_sub_one line 118
  24. theorem OAI.Erdos3.CircleFourier.two_mul_integerDistance_mul_norm_geometricCharacterSum_le_one line 154
  25. theorem OAI.Erdos3.CircleFourier.norm_geometricCharacterSum_le line 165
  26. theorem OAI.Erdos3.CircleFourier.geometricCharacterSum_eq_sum_fin line 173
  27. def OAI.Erdos3.CircleFourier.characterLipConstant line 192
  28. theorem OAI.Erdos3.CircleFourier.coe_characterLipConstant line 194
  29. theorem OAI.Erdos3.CircleFourier.character_coe_exp line 196
  30. theorem OAI.Erdos3.CircleFourier.norm_character_sub_one_le line 204
  31. theorem OAI.Erdos3.CircleFourier.character_lipschitz line 219
  32. def OAI.Erdos3.cyclicIntegerCharacter line 242
  33. theorem OAI.Erdos3.cyclicIntegerCharacter_intCast line 248
  34. theorem OAI.Erdos3.cyclicIntegerCharacter_eq_zero_iff line 255
  35. theorem OAI.Erdos3.cyclicIntegerCharacter_sum line 269
  36. def OAI.Erdos3.gridResidueEquiv line 276
  37. def OAI.Erdos3.integerGridCharacter line 284
  38. theorem OAI.Erdos3.integerGridCharacter_eq line 287
  39. theorem OAI.Erdos3.integerGridCharacter_sum line 294
  40. def OAI.Erdos3.linearCircleHom line 312
  41. theorem OAI.Erdos3.integral_subgroup_le_linearCircleHom_ker line 315
  42. def OAI.Erdos3.quotientLinearPhase line 323
  43. def OAI.Erdos3.quotientLinearCharacter line 327
  44. theorem OAI.Erdos3.quotientLinearCharacter_mk line 331
  45. theorem OAI.Erdos3.quotientLinearCharacter_add line 336
  46. theorem OAI.Erdos3.quotientLinearCharacter_norm line 342
  47. theorem OAI.Erdos3.quotientLinearCharacter_zero line 346
  48. theorem OAI.Erdos3.quotientLinearCharacter_continuous line 352
  49. theorem OAI.Erdos3.linear_site_sum line 372
  50. theorem OAI.Erdos3.character_real_sum line 380
  51. def OAI.Erdos3.siteFunctionalCharacter line 389
  52. theorem OAI.Erdos3.siteFunctionalCharacter_norm line 393
  53. theorem OAI.Erdos3.character_linear_site_sum line 397
  54. theorem OAI.Erdos3.abs_linearMap_le_basis_bound line 414
  55. theorem OAI.Erdos3.norm_character_real_sub_one_le line 433
  56. theorem OAI.Erdos3.circle_coe_fintype_sum line 453
  57. def OAI.Erdos3.rectangularGridCharacter line 457
  58. def OAI.Erdos3.integerGridResidue line 461
  59. theorem OAI.Erdos3.rectangularGridCharacter_eq line 463
  60. theorem OAI.Erdos3.rectangularGridCharacter_norm line 469
  61. theorem OAI.Erdos3.rectangularGridCharacter_add line 474
  62. theorem OAI.Erdos3.rectangularGridCharacter_sub line 481
  63. theorem OAI.Erdos3.rectangularGridCharacter_fintype_sum line 488
  64. theorem OAI.Erdos3.rectangularGridCharacter_sum line 496
  65. theorem OAI.Erdos3.rectangularGridCharacter_orthogonality line 514