OAI/Combinatorics/SquareDifference/CompleteWeights.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.coordinateChar_inflation_trivial line 10
  2. def OAI.SquareDifference.primaryModulus line 28
  3. lemma OAI.SquareDifference.primaryModulus_of_dvd line 30
  4. lemma OAI.SquareDifference.primaryModulus_of_not_dvd line 35
  5. lemma OAI.SquareDifference.primaryModulus_pos line 38
  6. lemma OAI.SquareDifference.primaryModulus_le line 40
  7. lemma OAI.SquareDifference.primaryModulus_dvd line 44
  8. lemma OAI.SquareDifference.primaryModulus_coprime line 47
  9. lemma OAI.SquareDifference.primaryModulus_pairwise line 52
  10. lemma OAI.SquareDifference.dvd_primaryModulus_product line 59
  11. lemma OAI.SquareDifference.prime_dvd_primaryModulus line 71
  12. lemma OAI.SquareDifference.primaryModulus_eq_or_square line 74
  13. lemma OAI.SquareDifference.primaryModulus_eq_of_dvd_prime line 82
  14. lemma OAI.SquareDifference.primaryModulus_two_small_or_large line 86
  15. lemma OAI.SquareDifference.primaryModulus_odd_unit_two line 96
  16. instance OAI.SquareDifference.primaryModulus_neZero line 102
  17. lemma OAI.SquareDifference.primary_root_odd_zero line 105
  18. lemma OAI.SquareDifference.primary_root_two_zero line 116
  19. lemma OAI.SquareDifference.primary_sieve_square_zero line 123
  20. def OAI.SquareDifference.expPhase line 132
  21. def OAI.SquareDifference.periodicMean line 134
  22. lemma OAI.SquareDifference.rational_num_isUnit line 136
  23. def OAI.SquareDifference.rationalChar line 142
  24. lemma OAI.SquareDifference.rationalChar_primitive line 145
  25. lemma OAI.SquareDifference.rationalChar_int line 149
  26. lemma OAI.SquareDifference.rationalChar_nat_square line 159
  27. lemma OAI.SquareDifference.finEquiv_natCast line 169
  28. lemma OAI.SquareDifference.expect_zmod_range line 177
  29. lemma OAI.SquareDifference.periodicMean_shift_one line 184
  30. lemma OAI.SquareDifference.zmod_natCast_periodic line 191
  31. lemma OAI.SquareDifference.periodicMean_factor_expect line 196
  32. lemma OAI.SquareDifference.rational_periodic_coefficient line 205
  33. def OAI.SquareDifference.localRootWeight line 228
  34. def OAI.SquareDifference.localSieveWeight line 231
  35. lemma OAI.SquareDifference.localRootWeight_natCast line 235
  36. lemma OAI.SquareDifference.localSieveWeight_natCast line 243
  37. lemma OAI.SquareDifference.crt_root_sieve_coefficient line 249
  38. lemma OAI.SquareDifference.periodicMean_crt_root_sieve line 268
  39. lemma OAI.SquareDifference.primaryModuli_pairwise line 298
  40. lemma OAI.SquareDifference.primary_two_root_zero_of_eq line 306
  41. def OAI.SquareDifference.primaryCoordinateChar line 322
  42. lemma OAI.SquareDifference.primaryCoordinateChar_primitive line 327
  43. lemma OAI.SquareDifference.primaryCoordinateChar_trivial line 333
  44. def OAI.SquareDifference.primaryActive line 338
  45. lemma OAI.SquareDifference.mem_primaryActive line 341
  46. lemma OAI.SquareDifference.primary_root_sieve_decay line 344
  47. lemma OAI.SquareDifference.primary_root_sieve_odd_zero line 364
  48. lemma OAI.SquareDifference.primary_root_sieve_square_zero line 381
  49. lemma OAI.SquareDifference.primary_root_sieve_complete line 400
  50. lemma OAI.SquareDifference.primary_root_sieve_tail line 423
  51. lemma OAI.SquareDifference.primary_root_sieve_two_zero line 438
  52. lemma OAI.SquareDifference.nat_pairwise_coprime_prod_dvd line 457
  53. lemma OAI.SquareDifference.primary_denominator_factor line 474
  54. lemma OAI.SquareDifference.primary_denominator_root_factor line 492
  55. def OAI.SquareDifference.primarySieveCoefficient line 506
  56. def OAI.SquareDifference.primaryModelCoefficient line 515
  57. lemma OAI.SquareDifference.primary_coefficient_small line 526
  58. lemma OAI.SquareDifference.primary_coefficient_uniform line 545
  59. def OAI.SquareDifference.actualRootWeight line 559
  60. def OAI.SquareDifference.actualSieveWeight line 562
  61. def OAI.SquareDifference.actualDivisorWeight line 565
  62. lemma OAI.SquareDifference.actualRootWeight_local line 571
  63. lemma OAI.SquareDifference.actualSieveWeight_local line 580
  64. lemma OAI.SquareDifference.actualDivisorWeight_coefficient line 586
  65. lemma OAI.SquareDifference.actualDivisorWeight_coefficient_uniform line 612
  66. def OAI.SquareDifference.rootSquareModulus line 620
  67. lemma OAI.SquareDifference.rootSquareModulus_pos line 623
  68. lemma OAI.SquareDifference.unitQuadraticMean_norm line 630
  69. lemma OAI.SquareDifference.primaryModelCoefficient_norm line 637
  70. lemma OAI.SquareDifference.primaryModelCoefficient_denominator line 653
  71. lemma OAI.SquareDifference.primaryModelCoefficient_denominator_le line 694
  72. lemma OAI.SquareDifference.primaryModelCoefficient_zero_of_denominator line 710