OAI/Combinatorics/SquareDifference/CircleDistance.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.periodic_nat_mod line 10
  2. lemma OAI.SquareDifference.periodic_sum_multiple line 15
  3. lemma OAI.SquareDifference.periodicMean_multiple line 27
  4. lemma OAI.SquareDifference.periodicMean_of_dvd line 33
  5. lemma OAI.SquareDifference.periodicMean_independent line 41
  6. lemma OAI.SquareDifference.periodicMean_sum line 49
  7. lemma OAI.SquareDifference.periodicMean_mul_left line 54
  8. lemma OAI.SquareDifference.prime_dvd_finset_prod_iff line 59
  9. lemma OAI.SquareDifference.mem_iff_dvd_prime_product line 68
  10. lemma OAI.SquareDifference.prime_product_injective line 78
  11. lemma OAI.SquareDifference.bounded_prime_subsets_card line 86
  12. lemma OAI.SquareDifference.hasFourierBound_zero line 106
  13. lemma OAI.SquareDifference.HasFourierBound.mono line 110
  14. lemma OAI.SquareDifference.HasFourierBound.mul_left line 116
  15. lemma OAI.SquareDifference.hasFourierBound_sum line 127
  16. lemma OAI.SquareDifference.hasFourierBound_prod_budget line 149
  17. lemma OAI.SquareDifference.actualRootWeight_norm line 166
  18. lemma OAI.SquareDifference.actualSieveWeight_norm line 174
  19. lemma OAI.SquareDifference.actualRootWeight_periodic line 184
  20. lemma OAI.SquareDifference.actualSieveWeight_periodic line 193
  21. lemma OAI.SquareDifference.actualTermWeight_periodic line 202
  22. def OAI.SquareDifference.ringRootWeight line 215
  23. def OAI.SquareDifference.ringSieveWeight line 218
  24. def OAI.SquareDifference.ringDivisorWeight line 221
  25. lemma OAI.SquareDifference.ringRootWeight_natCast line 226
  26. lemma OAI.SquareDifference.ringSieveWeight_natCast line 232
  27. lemma OAI.SquareDifference.ringDivisorWeight_natCast line 237
  28. lemma OAI.SquareDifference.ringRootWeight_fourier line 242
  29. lemma OAI.SquareDifference.ringSieveWeight_fourier line 249
  30. lemma OAI.SquareDifference.ringDivisorWeight_fourier line 259
  31. def OAI.SquareDifference.actualCompleteWeight line 289
  32. lemma OAI.SquareDifference.prime_subset_product_le line 294
  33. lemma OAI.SquareDifference.actualDivisorWeight_complete line 298
  34. lemma OAI.SquareDifference.actualCompleteWeight_periodic line 307
  35. lemma OAI.SquareDifference.primaryModelCoefficient_complete line 320
  36. def OAI.SquareDifference.smallQuadraticModulus line 337
  37. lemma OAI.SquareDifference.smallQuadraticModulus_pos line 339
  38. instance OAI.SquareDifference.(instance at line 345) line 345
  39. lemma OAI.SquareDifference.prime_dvd_smallQuadraticModulus line 348
  40. lemma OAI.SquareDifference.smallQuadraticModuli_pairwise line 354
  41. def OAI.SquareDifference.smallRootSquare line 366
  42. lemma OAI.SquareDifference.small_root_quadratic line 369
  43. lemma OAI.SquareDifference.crt_complete_coefficient line 394
  44. lemma OAI.SquareDifference.periodicMean_crt_complete line 408
  45. def OAI.SquareDifference.circleDistance line 432
  46. lemma OAI.SquareDifference.expPhase_zero line 434
  47. lemma OAI.SquareDifference.norm_expPhase line 435
  48. lemma OAI.SquareDifference.expPhase_add line 437
  49. lemma OAI.SquareDifference.expPhase_neg line 440
  50. lemma OAI.SquareDifference.expPhase_sub line 443
  51. lemma OAI.SquareDifference.expPhase_nat_mul line 446
  52. lemma OAI.SquareDifference.expPhase_int line 450
  53. lemma OAI.SquareDifference.expPhase_sub_int line 456
  54. lemma OAI.SquareDifference.circleDistance_nonneg line 459
  55. lemma OAI.SquareDifference.circleDistance_le_half line 461
  56. lemma OAI.SquareDifference.circleDistance_le_abs_sub_int line 463
  57. lemma OAI.SquareDifference.circleDistance_le_abs line 466
  58. lemma OAI.SquareDifference.circleDistance_sub_le line 469
  59. lemma OAI.SquareDifference.expPhase_sub_one_lower line 476
  60. lemma OAI.SquareDifference.linear_phase_sum_trivial line 492
  61. lemma OAI.SquareDifference.linear_phase_sum_distance line 498
  62. def OAI.SquareDifference.phaseBound line 516
  63. lemma OAI.SquareDifference.phaseBound_nonneg line 519
  64. lemma OAI.SquareDifference.phaseBound_le line 525