OAI/Combinatorics/SquareDifference/FourierLift.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LiftAnalysis.SquareDifference.symmetrization_moment line 13
  2. lemma OAI.LiftAnalysis.SquareDifference.sum_pow_tuples line 81
  3. lemma OAI.LiftAnalysis.SquareDifference.expect_condition line 86
  4. lemma OAI.LiftAnalysis.SquareDifference.square_moment_step line 99
  5. lemma OAI.LiftAnalysis.SquareDifference.square_moment_bound line 145
  6. lemma OAI.LiftAnalysis.SquareDifference.synthesis_norm_sq_bound line 174
  7. lemma OAI.LiftAnalysis.SquareDifference.analysis_of_synthesis line 214
  8. def OAI.LiftAnalysis.SquareDifference.expPhase line 244
  9. def OAI.LiftAnalysis.SquareDifference.circleDistance line 246
  10. lemma OAI.LiftAnalysis.SquareDifference.expPhase_zero line 248
  11. lemma OAI.LiftAnalysis.SquareDifference.norm_expPhase line 249
  12. lemma OAI.LiftAnalysis.SquareDifference.expPhase_add line 251
  13. lemma OAI.LiftAnalysis.SquareDifference.expPhase_neg line 254
  14. lemma OAI.LiftAnalysis.SquareDifference.expPhase_sub line 257
  15. lemma OAI.LiftAnalysis.SquareDifference.expPhase_nat_mul line 260
  16. lemma OAI.LiftAnalysis.SquareDifference.expPhase_int line 264
  17. lemma OAI.LiftAnalysis.SquareDifference.expPhase_sub_int line 270
  18. lemma OAI.LiftAnalysis.SquareDifference.circleDistance_nonneg line 273
  19. lemma OAI.LiftAnalysis.SquareDifference.circleDistance_le_half line 275
  20. lemma OAI.LiftAnalysis.SquareDifference.circleDistance_le_abs_sub_int line 277
  21. lemma OAI.LiftAnalysis.SquareDifference.circleDistance_le_abs line 280
  22. lemma OAI.LiftAnalysis.SquareDifference.circleDistance_sub_le line 283
  23. lemma OAI.LiftAnalysis.SquareDifference.expPhase_sub_one_lower line 290
  24. lemma OAI.LiftAnalysis.SquareDifference.linear_phase_sum_trivial line 306
  25. lemma OAI.LiftAnalysis.SquareDifference.linear_phase_sum_distance line 312
  26. lemma OAI.LiftAnalysis.SquareDifference.finite_phase_analysis line 330
  27. lemma OAI.LiftAnalysis.SquareDifference.finite_phase_analysis_average line 368
  28. lemma OAI.LiftAnalysis.SquareDifference.stdAddChar_eq_expPhase line 382
  29. lemma OAI.LiftAnalysis.SquareDifference.expPhase_sum line 390
  30. abbrev OAI.LiftAnalysis.SquareDifference.ResidueSpace line 401
  31. def OAI.LiftAnalysis.SquareDifference.prodChar line 403
  32. def OAI.LiftAnalysis.SquareDifference.frequencyAngle line 406
  33. def OAI.LiftAnalysis.SquareDifference.primeSupport line 409
  34. def OAI.LiftAnalysis.SquareDifference.supportDenominator line 412
  35. lemma OAI.LiftAnalysis.SquareDifference.prodChar_zero line 415
  36. lemma OAI.LiftAnalysis.SquareDifference.prodChar_zero_right line 417
  37. lemma OAI.LiftAnalysis.SquareDifference.prodChar_add line 419
  38. lemma OAI.LiftAnalysis.SquareDifference.prodChar_add_right line 422
  39. lemma OAI.LiftAnalysis.SquareDifference.prodChar_neg line 425
  40. lemma OAI.LiftAnalysis.SquareDifference.prodChar_sub line 427
  41. lemma OAI.LiftAnalysis.SquareDifference.prodChar_symm line 430
  42. lemma OAI.LiftAnalysis.SquareDifference.norm_prodChar line 432
  43. lemma OAI.LiftAnalysis.SquareDifference.prodChar_nat_diagonal line 434
  44. lemma OAI.LiftAnalysis.SquareDifference.prodChar_one_diagonal line 442
  45. lemma OAI.LiftAnalysis.SquareDifference.prodChar_eq_one_iff line 446
  46. lemma OAI.LiftAnalysis.SquareDifference.frequencyAngle_separates line 465
  47. lemma OAI.LiftAnalysis.SquareDifference.complex_expect_prod_pi line 488
  48. lemma OAI.LiftAnalysis.SquareDifference.prime_char_expect line 497
  49. lemma OAI.LiftAnalysis.SquareDifference.prodChar_expect line 505
  50. lemma OAI.LiftAnalysis.SquareDifference.prodChar_orthogonal line 520
  51. def OAI.LiftAnalysis.SquareDifference.supportNumerator line 526
  52. lemma OAI.LiftAnalysis.SquareDifference.supportDenominator_pos line 530
  53. lemma OAI.LiftAnalysis.SquareDifference.frequencyAngle_numerator line 534
  54. lemma OAI.LiftAnalysis.SquareDifference.frequencyAngle_difference line 558
  55. lemma OAI.LiftAnalysis.SquareDifference.frequency_difference_not_dvd line 569
  56. lemma OAI.LiftAnalysis.SquareDifference.frequencyAngle_remainder line 585
  57. lemma OAI.LiftAnalysis.SquareDifference.bounded_frequency_card line 604
  58. lemma OAI.LiftAnalysis.SquareDifference.rational_circleDistance_lower line 635
  59. lemma OAI.LiftAnalysis.SquareDifference.frequency_spacing line 654
  60. lemma OAI.LiftAnalysis.SquareDifference.arithmetic_phase_analysis line 681
  61. def OAI.LiftAnalysis.SquareDifference.residueGate line 709
  62. lemma OAI.LiftAnalysis.SquareDifference.sum_char_nonzero line 712
  63. lemma OAI.LiftAnalysis.SquareDifference.exact_support_iff line 732
  64. lemma OAI.LiftAnalysis.SquareDifference.sum_char_exact line 736
  65. def OAI.LiftAnalysis.SquareDifference.exactGate line 766
  66. lemma OAI.LiftAnalysis.SquareDifference.exactGate_fourier line 769
  67. lemma OAI.LiftAnalysis.SquareDifference.prodChar_neg_right line 774
  68. lemma OAI.LiftAnalysis.SquareDifference.prodChar_sub_right line 777
  69. def OAI.LiftAnalysis.SquareDifference.fourierPolynomial line 781
  70. lemma OAI.LiftAnalysis.SquareDifference.prodChar_norm_sq line 784
  71. lemma OAI.LiftAnalysis.SquareDifference.fourierPolynomial_parseval line 789
  72. lemma OAI.LiftAnalysis.SquareDifference.fourierPolynomial_reconstruction line 805
  73. lemma OAI.LiftAnalysis.SquareDifference.residue_crt line 829
  74. lemma OAI.LiftAnalysis.SquareDifference.support_coprime line 867
  75. lemma OAI.LiftAnalysis.SquareDifference.product_indicator line 878
  76. lemma OAI.LiftAnalysis.SquareDifference.exactGate_expand line 893
  77. lemma OAI.LiftAnalysis.SquareDifference.vector_signed_sum_bound line 913
  78. lemma OAI.LiftAnalysis.SquareDifference.sum_residue_progression line 936
  79. lemma OAI.LiftAnalysis.SquareDifference.progression_analysis line 958
  80. lemma OAI.LiftAnalysis.SquareDifference.progression_normalized_bound line 1003
  81. def OAI.LiftAnalysis.SquareDifference.gateCoefficient line 1036
  82. lemma OAI.LiftAnalysis.SquareDifference.gateCoefficient_expand line 1042
  83. lemma OAI.LiftAnalysis.SquareDifference.gateCoefficient_bound line 1059
  84. def OAI.LiftAnalysis.SquareDifference.coordinateFreeze line 1102
  85. lemma OAI.LiftAnalysis.SquareDifference.exactGate_freeze line 1106
  86. lemma OAI.LiftAnalysis.SquareDifference.coordinateFreeze_sub line 1120
  87. def OAI.LiftAnalysis.SquareDifference.liftPiece line 1125
  88. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_freeze_fourier line 1129
  89. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_conditional_parseval line 1155
  90. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_fixed_intersection_bound line 1171
  91. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_conditional_square_sum line 1227
  92. lemma OAI.LiftAnalysis.SquareDifference.residueGate_expect line 1253
  93. lemma OAI.LiftAnalysis.SquareDifference.exactGate_update_mean line 1262
  94. lemma OAI.LiftAnalysis.SquareDifference.exactGate_update_outside line 1278
  95. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_exactSupport line 1287
  96. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_moment line 1296
  97. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_moment_small_loss line 1330
  98. lemma OAI.LiftAnalysis.SquareDifference.exponential_support_bound line 1382
  99. lemma OAI.LiftAnalysis.SquareDifference.exists_nat_power_threshold line 1420
  100. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_moment_uniform line 1425
  101. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_moment_subpower line 1481