OAI/NumberTheory/DirichletL/CubicSieve/Poisson.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CubicSieve.canonical_finite_prime_gauss_transform_scalar_of_nontrivial line 12
  2. theorem OAI.SevenEighths.CubicSieve.canonical_finite_prime_gauss_transform_conj_of_nontrivial line 30
  3. theorem OAI.SevenEighths.CubicSieve.canonical_principal_gauss_transform_of_nontrivial line 45
  4. theorem OAI.SevenEighths.CubicSieve.canonical_radial_poisson_of_nontrivial line 82
  5. theorem OAI.SevenEighths.CubicSieve.canonical_radial_poisson_normalized_of_nontrivial line 128
  6. theorem OAI.SevenEighths.CubicSieve.norm_canonicalGaussSum_of_nontrivial line 169
  7. theorem OAI.SevenEighths.CubicSieve.norm_canonicalNormalizedGauss_of_nontrivial line 202
  8. theorem OAI.SevenEighths.CubicSieve.canonical_polya_vinogradov_of_nontrivial line 217
  9. theorem OAI.SevenEighths.CubicSieve.canonical_masked_polya_vinogradov_of_nontrivial line 270
  10. def OAI.SevenEighths.CubicSieve.cubicExponent line 303
  11. theorem OAI.SevenEighths.CubicSieve.cubicExponent_nonprincipal line 305
  12. theorem OAI.SevenEighths.CubicSieve.cubic_radial_poisson line 331
  13. theorem OAI.SevenEighths.CubicSieve.cubic_polya_vinogradov line 346