OAI/Combinatorics/SquareDifference/PhaseBounds.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.linear_phase_sum_bound line 10
  2. def OAI.SquareDifference.distanceBucket line 21
  3. lemma OAI.SquareDifference.distanceBucket_le line 24
  4. lemma OAI.SquareDifference.distanceBucket_same_close line 29
  5. def OAI.SquareDifference.bucketWeight line 65
  6. lemma OAI.SquareDifference.phaseBound_le_bucketWeight line 68
  7. lemma OAI.SquareDifference.separated_phaseBound_sum line 88
  8. lemma OAI.SquareDifference.circleDistance_lipschitz line 131
  9. lemma OAI.SquareDifference.rational_circleDistance_lower line 137
  10. lemma OAI.SquareDifference.rational_quadratic_spacing line 156
  11. lemma OAI.SquareDifference.sum_range_blocks line 184
  12. lemma OAI.SquareDifference.quadratic_block_bound line 191
  13. lemma OAI.SquareDifference.rational_spacing_sum line 221
  14. lemma OAI.SquareDifference.sum_triangle_differences line 270
  15. lemma OAI.SquareDifference.complex_sum_square_identity line 296
  16. lemma OAI.SquareDifference.norm_sum_square_differencing line 312
  17. lemma OAI.SquareDifference.quadratic_correlation line 326
  18. lemma OAI.SquareDifference.phaseBound_mono line 335
  19. lemma OAI.SquareDifference.quadratic_sum_differencing line 342
  20. lemma OAI.SquareDifference.expPhase_lipschitz line 365
  21. lemma OAI.SquareDifference.periodic_zero_prefix line 374
  22. lemma OAI.SquareDifference.norm_periodicMean line 388
  23. lemma OAI.SquareDifference.periodic_prefix_error line 399
  24. lemma OAI.SquareDifference.norm_weighted_partial_bound line 415
  25. def OAI.SquareDifference.squareWeight line 435
  26. lemma OAI.SquareDifference.norm_squareWeight line 438
  27. lemma OAI.SquareDifference.squareWeight_difference line 443
  28. lemma OAI.SquareDifference.squareWeight_variation line 465
  29. lemma OAI.SquareDifference.periodic_squareWeight_error line 490