OAI/Combinatorics/SquareDifference/PrimeGauss.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.quadratic_gauss_ring line 13
  2. lemma OAI.SquareDifference.quadratic_gauss_zmod line 48
  3. lemma OAI.SquareDifference.expect_surjective_addHom line 61
  4. lemma OAI.SquareDifference.zmod_factor_zero line 76
  5. lemma OAI.SquareDifference.zmod_kernel_factor line 83
  6. lemma OAI.SquareDifference.quadratic_shift_cancellation line 94
  7. lemma OAI.SquareDifference.zmod_fiber_translation line 116
  8. lemma OAI.SquareDifference.fiber_gauss_zero line 125
  9. lemma OAI.SquareDifference.odd_fiber_gauss_zero line 169
  10. lemma OAI.SquareDifference.weighted_fiber_sum line 180
  11. lemma OAI.SquareDifference.gauss_zero_of_fiber line 190
  12. lemma OAI.SquareDifference.odd_unit_gauss_zero line 203
  13. lemma OAI.SquareDifference.four_unit_mul_two line 215
  14. lemma OAI.SquareDifference.two_unit_gauss_zero line 225
  15. lemma OAI.SquareDifference.quadratic_gauss_ring_linear line 236
  16. lemma OAI.SquareDifference.norm_quadratic_expect line 271
  17. lemma OAI.SquareDifference.fourier_weighted_gauss line 282
  18. def OAI.SquareDifference.primeSieveWeight line 302
  19. lemma OAI.SquareDifference.primeSieveWeight_fourier line 305
  20. lemma OAI.SquareDifference.primeSieveWeight_abs_le line 326
  21. lemma OAI.SquareDifference.primeSieveWeight_mean_zero line 338
  22. lemma OAI.SquareDifference.primeSieveWeight_unit_density line 346
  23. def OAI.SquareDifference.zmodScaleHom line 358
  24. lemma OAI.SquareDifference.zmodScaleHom_int line 366
  25. lemma OAI.SquareDifference.zmodScaleHom_nat line 370
  26. lemma OAI.SquareDifference.zmodScaleHom_injective line 374
  27. lemma OAI.SquareDifference.zmodScaleHom_mul line 382
  28. lemma OAI.SquareDifference.zmodScale_primitive line 394
  29. lemma OAI.SquareDifference.primeSieveWeight_fourier_char line 406
  30. def OAI.SquareDifference.HasFourierBound line 426
  31. lemma OAI.SquareDifference.hasFourierBound_of_expansion line 430
  32. lemma OAI.SquareDifference.hasFourierBound_one line 451
  33. lemma OAI.SquareDifference.HasFourierBound.mul line 457
  34. lemma OAI.SquareDifference.hasFourierBound_prod line 479
  35. lemma OAI.SquareDifference.primeSieveWeight_fourier_bound line 490