OAI/Combinatorics/SquareDifference/SievedFourier.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.HasFourierBound.gauss line 10
  2. lemma OAI.SquareDifference.primitive_transport line 19
  3. lemma OAI.SquareDifference.primitive_mulShift line 29
  4. def OAI.SquareDifference.coordinateChar line 37
  5. lemma OAI.SquareDifference.coordinateChar_apply line 41
  6. lemma OAI.SquareDifference.coordinateChar_primitive line 45
  7. lemma OAI.SquareDifference.addChar_finset_sum line 63
  8. lemma OAI.SquareDifference.additive_character_product line 70
  9. lemma OAI.SquareDifference.complex_expect_pi_prod line 84
  10. lemma OAI.SquareDifference.product_quadratic_mean line 91
  11. lemma OAI.SquareDifference.primeSieveWeight_fourier_dvd line 106
  12. lemma OAI.SquareDifference.fiber_gauss_zero_char line 115
  13. lemma OAI.SquareDifference.quadratic_mean_equiv line 166
  14. lemma OAI.SquareDifference.crt_quadratic_mean line 176
  15. lemma OAI.SquareDifference.fiber_sum_gauss_zero_char line 187
  16. lemma OAI.SquareDifference.gauss_zero_of_fiber_char line 210
  17. lemma OAI.SquareDifference.odd_unit_gauss_zero_char line 225
  18. lemma OAI.SquareDifference.two_unit_gauss_zero_char line 235
  19. lemma OAI.SquareDifference.finite_complete_sieve line 245
  20. lemma OAI.SquareDifference.zmodScale_primitive_general line 251
  21. def OAI.SquareDifference.residueDensity line 261
  22. lemma OAI.SquareDifference.residueDensity_fourier_bound line 264
  23. lemma OAI.SquareDifference.residueDensity_fourier_dvd line 288
  24. lemma OAI.SquareDifference.residueDensity_mean line 296
  25. lemma OAI.SquareDifference.residueDensity_self line 314
  26. lemma OAI.SquareDifference.residueDensity_self_quadratic line 319
  27. lemma OAI.SquareDifference.residueDensity_quadratic_zero line 334
  28. lemma OAI.SquareDifference.zmod_cast_comp line 345
  29. lemma OAI.SquareDifference.odd_square_eight line 349
  30. lemma OAI.SquareDifference.odd_square_of_dvd_eight line 354
  31. lemma OAI.SquareDifference.odd_root_quadratic_small line 363
  32. lemma OAI.SquareDifference.unit_four_iff_odd line 374
  33. lemma OAI.SquareDifference.odd_root_quadratic_large line 379
  34. def OAI.SquareDifference.localSieveTerm line 397
  35. def OAI.SquareDifference.truncatedSieveMean line 401
  36. lemma OAI.SquareDifference.localSieveTerm_norm line 405
  37. lemma OAI.SquareDifference.truncatedSieveMean_bound line 420
  38. lemma OAI.SquareDifference.truncatedSieveMean_complete line 436
  39. lemma OAI.SquareDifference.localSieveTerm_product line 451
  40. lemma OAI.SquareDifference.localSieveTerm_zero line 461
  41. lemma OAI.SquareDifference.quadratic_sieve_bounds line 467
  42. lemma OAI.SquareDifference.nonprime_sieve_mean_zero line 480
  43. def OAI.SquareDifference.unitQuadraticMean line 490
  44. lemma OAI.SquareDifference.prime_unit_quadratic line 493