OAI/Combinatorics/SquareDifference/ResidueFourier.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LiftTheory.SquareDifference.residueFourier line 25
  2. def OAI.LiftTheory.SquareDifference.squareMultiplier line 28
  3. def OAI.LiftTheory.SquareDifference.squarePairForm line 31
  4. lemma OAI.LiftTheory.SquareDifference.residueFourier_polynomial line 34
  5. lemma OAI.LiftTheory.SquareDifference.residueFourier_reconstruction line 41
  6. lemma OAI.LiftTheory.SquareDifference.residueFourier_parseval line 46
  7. lemma OAI.LiftTheory.SquareDifference.pair_polynomial line 50
  8. lemma OAI.LiftTheory.SquareDifference.squarePairForm_fourier line 74
  9. lemma OAI.LiftTheory.SquareDifference.squareMultiplier_product line 79
  10. lemma OAI.LiftTheory.SquareDifference.fourier_pair_tail line 85
  11. lemma OAI.LiftTheory.SquareDifference.quadratic_gauss_ring line 125
  12. lemma OAI.LiftTheory.SquareDifference.quadratic_gauss_zmod line 160
  13. lemma OAI.LiftTheory.SquareDifference.expect_surjective_addHom line 173
  14. lemma OAI.LiftTheory.SquareDifference.zmod_factor_zero line 188
  15. lemma OAI.LiftTheory.SquareDifference.zmod_kernel_factor line 195
  16. lemma OAI.LiftTheory.SquareDifference.quadratic_shift_cancellation line 206
  17. lemma OAI.LiftTheory.SquareDifference.zmod_fiber_translation line 228
  18. lemma OAI.LiftTheory.SquareDifference.fiber_gauss_zero line 237
  19. lemma OAI.LiftTheory.SquareDifference.odd_fiber_gauss_zero line 281
  20. lemma OAI.LiftTheory.SquareDifference.weighted_fiber_sum line 292
  21. lemma OAI.LiftTheory.SquareDifference.gauss_zero_of_fiber line 302
  22. lemma OAI.LiftTheory.SquareDifference.odd_unit_gauss_zero line 315
  23. lemma OAI.LiftTheory.SquareDifference.four_unit_mul_two line 327
  24. lemma OAI.LiftTheory.SquareDifference.two_unit_gauss_zero line 337
  25. lemma OAI.LiftTheory.SquareDifference.quadratic_gauss_ring_linear line 348
  26. lemma OAI.LiftTheory.SquareDifference.norm_quadratic_expect line 383
  27. lemma OAI.LiftTheory.SquareDifference.fourier_weighted_gauss line 394
  28. def OAI.LiftTheory.SquareDifference.primeSieveWeight line 414
  29. lemma OAI.LiftTheory.SquareDifference.primeSieveWeight_fourier line 417
  30. lemma OAI.LiftTheory.SquareDifference.primeSieveWeight_abs_le line 438
  31. lemma OAI.LiftTheory.SquareDifference.primeSieveWeight_mean_zero line 450
  32. lemma OAI.LiftTheory.SquareDifference.primeSieveWeight_unit_density line 458
  33. def OAI.LiftTheory.SquareDifference.zmodScaleHom line 470
  34. lemma OAI.LiftTheory.SquareDifference.zmodScaleHom_int line 478
  35. lemma OAI.LiftTheory.SquareDifference.zmodScaleHom_nat line 482
  36. lemma OAI.LiftTheory.SquareDifference.zmodScaleHom_injective line 486
  37. lemma OAI.LiftTheory.SquareDifference.zmodScaleHom_mul line 494
  38. lemma OAI.LiftTheory.SquareDifference.zmodScale_primitive line 506
  39. lemma OAI.LiftTheory.SquareDifference.primeSieveWeight_fourier_char line 518