OAI/Combinatorics/SquareDifference/RationalLift.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LiftTheory.SquareDifference.symmetrization_moment line 17
  2. lemma OAI.LiftTheory.SquareDifference.sum_pow_tuples line 85
  3. lemma OAI.LiftTheory.SquareDifference.expect_condition line 90
  4. lemma OAI.LiftTheory.SquareDifference.square_moment_step line 103
  5. lemma OAI.LiftTheory.SquareDifference.square_moment_bound line 149
  6. lemma OAI.LiftTheory.SquareDifference.synthesis_norm_sq_bound line 178
  7. lemma OAI.LiftTheory.SquareDifference.analysis_of_synthesis line 218
  8. def OAI.LiftTheory.SquareDifference.expPhase line 248
  9. def OAI.LiftTheory.SquareDifference.circleDistance line 250
  10. lemma OAI.LiftTheory.SquareDifference.expPhase_zero line 252
  11. lemma OAI.LiftTheory.SquareDifference.norm_expPhase line 253
  12. lemma OAI.LiftTheory.SquareDifference.expPhase_add line 255
  13. lemma OAI.LiftTheory.SquareDifference.expPhase_neg line 258
  14. lemma OAI.LiftTheory.SquareDifference.expPhase_sub line 261
  15. lemma OAI.LiftTheory.SquareDifference.expPhase_nat_mul line 264
  16. lemma OAI.LiftTheory.SquareDifference.expPhase_int line 268
  17. lemma OAI.LiftTheory.SquareDifference.expPhase_sub_int line 274
  18. lemma OAI.LiftTheory.SquareDifference.circleDistance_nonneg line 277
  19. lemma OAI.LiftTheory.SquareDifference.circleDistance_le_half line 279
  20. lemma OAI.LiftTheory.SquareDifference.circleDistance_le_abs_sub_int line 281
  21. lemma OAI.LiftTheory.SquareDifference.circleDistance_le_abs line 284
  22. lemma OAI.LiftTheory.SquareDifference.circleDistance_sub_le line 287
  23. lemma OAI.LiftTheory.SquareDifference.expPhase_sub_one_lower line 294
  24. lemma OAI.LiftTheory.SquareDifference.linear_phase_sum_trivial line 310
  25. lemma OAI.LiftTheory.SquareDifference.linear_phase_sum_distance line 316
  26. lemma OAI.LiftTheory.SquareDifference.finite_phase_analysis line 334
  27. lemma OAI.LiftTheory.SquareDifference.finite_phase_analysis_average line 372
  28. lemma OAI.LiftTheory.SquareDifference.stdAddChar_eq_expPhase line 386
  29. lemma OAI.LiftTheory.SquareDifference.expPhase_sum line 394
  30. abbrev OAI.LiftTheory.SquareDifference.ResidueSpace line 405
  31. def OAI.LiftTheory.SquareDifference.prodChar line 407
  32. def OAI.LiftTheory.SquareDifference.frequencyAngle line 410
  33. def OAI.LiftTheory.SquareDifference.primeSupport line 413
  34. def OAI.LiftTheory.SquareDifference.supportDenominator line 416
  35. lemma OAI.LiftTheory.SquareDifference.prodChar_zero line 419
  36. lemma OAI.LiftTheory.SquareDifference.prodChar_zero_right line 421
  37. lemma OAI.LiftTheory.SquareDifference.prodChar_add line 423
  38. lemma OAI.LiftTheory.SquareDifference.prodChar_add_right line 426
  39. lemma OAI.LiftTheory.SquareDifference.prodChar_neg line 429
  40. lemma OAI.LiftTheory.SquareDifference.prodChar_sub line 431
  41. lemma OAI.LiftTheory.SquareDifference.prodChar_symm line 434
  42. lemma OAI.LiftTheory.SquareDifference.norm_prodChar line 436
  43. lemma OAI.LiftTheory.SquareDifference.prodChar_nat_diagonal line 438
  44. lemma OAI.LiftTheory.SquareDifference.prodChar_one_diagonal line 446
  45. lemma OAI.LiftTheory.SquareDifference.prodChar_eq_one_iff line 450
  46. lemma OAI.LiftTheory.SquareDifference.frequencyAngle_separates line 469
  47. lemma OAI.LiftTheory.SquareDifference.complex_expect_prod_pi line 492
  48. lemma OAI.LiftTheory.SquareDifference.prime_char_expect line 501
  49. lemma OAI.LiftTheory.SquareDifference.prodChar_expect line 509
  50. lemma OAI.LiftTheory.SquareDifference.prodChar_orthogonal line 524
  51. def OAI.LiftTheory.SquareDifference.supportNumerator line 530
  52. lemma OAI.LiftTheory.SquareDifference.supportDenominator_pos line 534
  53. lemma OAI.LiftTheory.SquareDifference.frequencyAngle_numerator line 538
  54. lemma OAI.LiftTheory.SquareDifference.frequencyAngle_difference line 562
  55. lemma OAI.LiftTheory.SquareDifference.frequency_difference_not_dvd line 573
  56. lemma OAI.LiftTheory.SquareDifference.frequencyAngle_remainder line 589
  57. lemma OAI.LiftTheory.SquareDifference.bounded_frequency_card line 608
  58. lemma OAI.LiftTheory.SquareDifference.rational_circleDistance_lower line 639
  59. lemma OAI.LiftTheory.SquareDifference.frequency_spacing line 658
  60. lemma OAI.LiftTheory.SquareDifference.arithmetic_phase_analysis line 685
  61. def OAI.LiftTheory.SquareDifference.residueGate line 713
  62. lemma OAI.LiftTheory.SquareDifference.sum_char_nonzero line 716
  63. lemma OAI.LiftTheory.SquareDifference.exact_support_iff line 736
  64. lemma OAI.LiftTheory.SquareDifference.sum_char_exact line 740
  65. def OAI.LiftTheory.SquareDifference.exactGate line 770
  66. lemma OAI.LiftTheory.SquareDifference.exactGate_fourier line 773
  67. lemma OAI.LiftTheory.SquareDifference.prodChar_neg_right line 778
  68. lemma OAI.LiftTheory.SquareDifference.prodChar_sub_right line 781
  69. def OAI.LiftTheory.SquareDifference.fourierPolynomial line 785
  70. lemma OAI.LiftTheory.SquareDifference.prodChar_norm_sq line 788
  71. lemma OAI.LiftTheory.SquareDifference.fourierPolynomial_parseval line 793
  72. lemma OAI.LiftTheory.SquareDifference.fourierPolynomial_reconstruction line 809
  73. lemma OAI.LiftTheory.SquareDifference.residue_crt line 833
  74. lemma OAI.LiftTheory.SquareDifference.support_coprime line 871
  75. lemma OAI.LiftTheory.SquareDifference.product_indicator line 882
  76. lemma OAI.LiftTheory.SquareDifference.exactGate_expand line 897
  77. lemma OAI.LiftTheory.SquareDifference.vector_signed_sum_bound line 917
  78. lemma OAI.LiftTheory.SquareDifference.sum_residue_progression line 940
  79. lemma OAI.LiftTheory.SquareDifference.progression_analysis line 962
  80. lemma OAI.LiftTheory.SquareDifference.progression_normalized_bound line 1007
  81. def OAI.LiftTheory.SquareDifference.gateCoefficient line 1040
  82. lemma OAI.LiftTheory.SquareDifference.gateCoefficient_expand line 1046
  83. lemma OAI.LiftTheory.SquareDifference.gateCoefficient_bound line 1063
  84. def OAI.LiftTheory.SquareDifference.coordinateFreeze line 1106
  85. lemma OAI.LiftTheory.SquareDifference.exactGate_freeze line 1110
  86. lemma OAI.LiftTheory.SquareDifference.coordinateFreeze_sub line 1124
  87. def OAI.LiftTheory.SquareDifference.liftPiece line 1129
  88. lemma OAI.LiftTheory.SquareDifference.liftPiece_freeze_fourier line 1133
  89. lemma OAI.LiftTheory.SquareDifference.liftPiece_conditional_parseval line 1159
  90. lemma OAI.LiftTheory.SquareDifference.liftPiece_fixed_intersection_bound line 1175
  91. lemma OAI.LiftTheory.SquareDifference.liftPiece_conditional_square_sum line 1231
  92. lemma OAI.LiftTheory.SquareDifference.residueGate_expect line 1257
  93. lemma OAI.LiftTheory.SquareDifference.exactGate_update_mean line 1266
  94. lemma OAI.LiftTheory.SquareDifference.exactGate_update_outside line 1282
  95. lemma OAI.LiftTheory.SquareDifference.liftPiece_exactSupport line 1291
  96. lemma OAI.LiftTheory.SquareDifference.liftPiece_moment line 1300
  97. lemma OAI.LiftTheory.SquareDifference.liftPiece_moment_small_loss line 1334
  98. lemma OAI.LiftTheory.SquareDifference.exponential_support_bound line 1386
  99. lemma OAI.LiftTheory.SquareDifference.exists_nat_power_threshold line 1424
  100. lemma OAI.LiftTheory.SquareDifference.liftPiece_moment_uniform line 1429
  101. lemma OAI.LiftTheory.SquareDifference.liftPiece_moment_subpower line 1485