OAI/NumberTheory/DirichletL/GaussSum/CompletedExpansion.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompletedGauss.expandedTerm line 78
  2. theorem OAI.CompletedGauss.finite_support_expandedTerm line 84
  3. theorem OAI.CompletedGauss.expandedTerm_scale line 94
  4. theorem OAI.CompletedGauss.expandedTerm_one line 106
  5. theorem OAI.CompletedGauss.completedT_finite_support line 112
  6. theorem OAI.CompletedGauss.completedT_summable line 123
  7. theorem OAI.CompletedGauss.weighted_completedT_reopen line 128
  8. theorem OAI.CompletedGauss.cube_inverse_finite_support line 134
  9. theorem OAI.CompletedGauss.cube_inner_inverse line 152
  10. theorem OAI.CompletedGauss.completed_cube_inverse_vstar line 174
  11. theorem OAI.CompletedGauss.vstar_source_normalization line 204
  12. theorem OAI.CompletedGauss.completed_cube_inverse line 218
  13. theorem OAI.CompletedGauss.normalizedFactors_product line 231
  14. theorem OAI.CompletedGauss.product_primary line 245
  15. def OAI.CompletedGauss.productPrimeIndexEquiv line 252
  16. theorem OAI.CompletedGauss.cubicRow_product_mk line 276
  17. theorem OAI.CompletedGauss.gaussTwo_eq_canonicalProductGauss line 289
  18. theorem OAI.CompletedGauss.squarefreeGaussCoefficient_eq_canonicalProductCoefficient line 329
  19. def OAI.FiniteRayExpansion.unitFourierCoeff line 361
  20. theorem OAI.FiniteRayExpansion.unit_fourier_inversion line 364
  21. theorem OAI.FiniteRayExpansion.norm_char_unit line 373
  22. theorem OAI.FiniteRayExpansion.norm_char_le_one line 377
  23. theorem OAI.FiniteRayExpansion.unitFourierCoeff_norm_le_average line 384
  24. theorem OAI.FiniteRayExpansion.unitFourierCoeff_norm_le line 392
  25. theorem OAI.FiniteRayExpansion.character_card_eq_units line 401
  26. theorem OAI.FiniteRayExpansion.unitFourierCoeff_sum_norm_le line 405
  27. theorem OAI.FiniteRayExpansion.unitFourierCoeff_sum_norm_le_sum line 413
  28. def OAI.FiniteRayExpansion.zeroExtendUnits line 423
  29. theorem OAI.FiniteRayExpansion.zeroExtendUnits_unit line 426
  30. theorem OAI.FiniteRayExpansion.zeroExtendUnits_nonunit line 432
  31. theorem OAI.FiniteRayExpansion.zeroExtendUnits_fourier line 435
  32. theorem OAI.FiniteRayExpansion.zeroExtendUnits_restrict line 444
  33. def OAI.FiniteRayExpansion.unitTensorCoeff line 451
  34. theorem OAI.FiniteRayExpansion.unit_tensor_fourier_inversion line 454
  35. theorem OAI.FiniteRayExpansion.unitTensorCoeff_norm_le line 470
  36. theorem OAI.FiniteRayExpansion.unitTensorCoeff_sum_norm_le line 475
  37. theorem OAI.FiniteRayExpansion.unitTensorCoeff_sum_norm_le_sum line 486
  38. def OAI.FiniteRayExpansion.zeroExtendUnitPair line 496
  39. theorem OAI.FiniteRayExpansion.zeroExtendUnitPair_fourier line 499
  40. theorem OAI.FiniteRayExpansion.zeroExtendUnitPair_restrict line 513
  41. abbrev OAI.RayFourExpansion.O line 527
  42. abbrev OAI.RayFourExpansion.RayRing line 531
  43. instance OAI.RayFourExpansion.rayRingFintype line 533
  44. abbrev OAI.RayFourExpansion.RayCharacter line 537
  45. instance OAI.RayFourExpansion.rayCharacterFintype line 538
  46. def OAI.RayFourExpansion.rayCharacter line 540
  47. theorem OAI.RayFourExpansion.rayCharacter_mul line 543
  48. theorem OAI.RayFourExpansion.rayCharacter_eq_of_mod_four line 547
  49. def OAI.RayFourExpansion.rayMask line 553
  50. theorem OAI.RayFourExpansion.rayRing_card line 556
  51. theorem OAI.RayFourExpansion.rayUnit_card_le line 560
  52. theorem OAI.RayFourExpansion.rayCharacter_card_le line 565
  53. def OAI.RayFourExpansion.phaseCoeff line 569
  54. theorem OAI.RayFourExpansion.phase_expansion line 572
  55. theorem OAI.RayFourExpansion.phaseCoeff_norm_le line 578
  56. theorem OAI.RayFourExpansion.phaseCoeff_sum_norm_le line 582
  57. def OAI.RayFourExpansion.pairCoeff line 589
  58. theorem OAI.RayFourExpansion.pair_phase_expansion line 592
  59. theorem OAI.RayFourExpansion.pairCoeff_norm_le line 601
  60. theorem OAI.RayFourExpansion.pairCoeff_sum_norm_le line 605
  61. theorem OAI.RayFourExpansion.quadraticRayValue_bounds line 614
  62. theorem OAI.RayFourExpansion.fixedGQuotientValue_norm_le_two line 623
  63. def OAI.RayFourExpansion.gCoeff line 636
  64. theorem OAI.RayFourExpansion.gCoeff_norm_le_two line 638
  65. theorem OAI.RayFourExpansion.gCoeff_sum_norm_le line 641
  66. theorem OAI.RayFourExpansion.fixedG_character_expansion line 644
  67. def OAI.RayFourExpansion.crossQuotientPhase line 648
  68. theorem OAI.RayFourExpansion.crossQuotientPhase_norm_le_two line 651
  69. def OAI.RayFourExpansion.crossCoeff line 662
  70. theorem OAI.RayFourExpansion.crossCoeff_norm_le_two line 664
  71. theorem OAI.RayFourExpansion.crossCoeff_sum_norm_le line 667
  72. theorem OAI.RayFourExpansion.quadraticRayPair_character_expansion line 671