OAI/Combinatorics/SquareDifference/ConductorBounds.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LiftTheory.SquareDifference.HasFourierBound line 17
  2. lemma OAI.LiftTheory.SquareDifference.hasFourierBound_of_expansion line 21
  3. lemma OAI.LiftTheory.SquareDifference.hasFourierBound_one line 42
  4. lemma OAI.LiftTheory.SquareDifference.HasFourierBound.mul line 48
  5. lemma OAI.LiftTheory.SquareDifference.hasFourierBound_prod line 70
  6. lemma OAI.LiftTheory.SquareDifference.primeSieveWeight_fourier_bound line 81
  7. lemma OAI.LiftTheory.SquareDifference.HasFourierBound.gauss line 113
  8. lemma OAI.LiftTheory.SquareDifference.primitive_transport line 122
  9. lemma OAI.LiftTheory.SquareDifference.primitive_mulShift line 132
  10. def OAI.LiftTheory.SquareDifference.coordinateChar line 140
  11. lemma OAI.LiftTheory.SquareDifference.coordinateChar_apply line 144
  12. lemma OAI.LiftTheory.SquareDifference.coordinateChar_primitive line 148
  13. lemma OAI.LiftTheory.SquareDifference.addChar_finset_sum line 166
  14. lemma OAI.LiftTheory.SquareDifference.additive_character_product line 173
  15. lemma OAI.LiftTheory.SquareDifference.complex_expect_pi_prod line 187
  16. lemma OAI.LiftTheory.SquareDifference.product_quadratic_mean line 194
  17. lemma OAI.LiftTheory.SquareDifference.primeSieveWeight_fourier_dvd line 209
  18. lemma OAI.LiftTheory.SquareDifference.fiber_gauss_zero_char line 218
  19. lemma OAI.LiftTheory.SquareDifference.quadratic_mean_equiv line 269
  20. lemma OAI.LiftTheory.SquareDifference.crt_quadratic_mean line 279
  21. lemma OAI.LiftTheory.SquareDifference.fiber_sum_gauss_zero_char line 290
  22. lemma OAI.LiftTheory.SquareDifference.gauss_zero_of_fiber_char line 313
  23. lemma OAI.LiftTheory.SquareDifference.odd_unit_gauss_zero_char line 328
  24. lemma OAI.LiftTheory.SquareDifference.two_unit_gauss_zero_char line 338
  25. lemma OAI.LiftTheory.SquareDifference.finite_complete_sieve line 348
  26. lemma OAI.LiftTheory.SquareDifference.zmodScale_primitive_general line 354
  27. def OAI.LiftTheory.SquareDifference.residueDensity line 364
  28. lemma OAI.LiftTheory.SquareDifference.residueDensity_fourier_bound line 367
  29. lemma OAI.LiftTheory.SquareDifference.residueDensity_fourier_dvd line 391
  30. lemma OAI.LiftTheory.SquareDifference.residueDensity_mean line 399
  31. lemma OAI.LiftTheory.SquareDifference.residueDensity_self line 417
  32. lemma OAI.LiftTheory.SquareDifference.residueDensity_self_quadratic line 422
  33. lemma OAI.LiftTheory.SquareDifference.residueDensity_quadratic_zero line 437
  34. lemma OAI.LiftTheory.SquareDifference.zmod_cast_comp line 448
  35. lemma OAI.LiftTheory.SquareDifference.odd_square_eight line 452
  36. lemma OAI.LiftTheory.SquareDifference.odd_square_of_dvd_eight line 457
  37. lemma OAI.LiftTheory.SquareDifference.odd_root_quadratic_small line 466
  38. lemma OAI.LiftTheory.SquareDifference.unit_four_iff_odd line 477
  39. lemma OAI.LiftTheory.SquareDifference.odd_root_quadratic_large line 482
  40. def OAI.LiftTheory.SquareDifference.localSieveTerm line 500
  41. def OAI.LiftTheory.SquareDifference.truncatedSieveMean line 504
  42. lemma OAI.LiftTheory.SquareDifference.localSieveTerm_norm line 508