OAI/NumberTheory/DirichletL/Eisenstein/ConstantDirichletSeries.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.constant_dirichlet_support line 79
  2. lemma OAI.CubicEisenstein.totient_sum_good line 93
  3. lemma OAI.CubicEisenstein.norm_ramifiedRatio_lt_one line 105
  4. theorem OAI.CubicEisenstein.constantDirichlet_summable_norm line 112
  5. lemma OAI.CubicEisenstein.ramified_geometric_sum line 145
  6. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_zero_totient line 161
  7. theorem OAI.CubicEisenstein.scatteringCoefficient_zero_zeta line 197
  8. theorem OAI.CubicEisenstein.eisensteinConstantCoefficient_zeta line 209
  9. theorem OAI.CanonicalQuadraticSieve.matrix_eq_primePool line 223
  10. theorem OAI.CanonicalQuadraticSieve.sieveNorm_reverse_le line 238
  11. def OAI.CanonicalQuadraticSieve.dualPrincipalIdeal line 266
  12. def OAI.CanonicalQuadraticSieve.dualPrincipalLattice line 271
  13. theorem OAI.CanonicalQuadraticSieve.idealZeroMask_pair_zero line 275
  14. theorem OAI.CanonicalQuadraticSieve.dualPrincipalIdeal_eq_lattice line 282
  15. theorem OAI.CanonicalQuadraticSieve.dualPrincipalIdeal_truncated line 315
  16. theorem OAI.CanonicalQuadraticSieve.canonical_pair_ideal_fourier_summable line 337
  17. theorem OAI.CanonicalQuadraticSieve.canonical_nonprincipal_dual_principal line 349
  18. def OAI.CanonicalQuadraticSieve.canonicalMainBoundary line 403
  19. theorem OAI.CanonicalQuadraticSieve.canonicalMainBoundary_bound line 414
  20. theorem OAI.CanonicalQuadraticSieve.canonicalMainBoundary_small_power line 439
  21. theorem OAI.CanonicalQuadraticSieve.canonicalMainBoundary_reverse line 454
  22. def OAI.CanonicalQuadraticSieve.CoefficientOnShell line 474
  23. theorem OAI.CanonicalQuadraticSieve.column_dyadic_exists line 477
  24. def OAI.CanonicalQuadraticSieve.columnDyadicSector line 484
  25. def OAI.CanonicalQuadraticSieve.dyadicColumnCoefficient line 488
  26. theorem OAI.CanonicalQuadraticSieve.dyadicColumnCoefficient_shell line 492
  27. theorem OAI.CanonicalQuadraticSieve.dyadicColumnCoefficient_energy line 504
  28. theorem OAI.CanonicalQuadraticSieve.weighted_energy_column_shells line 509
  29. theorem OAI.CanonicalQuadraticSieve.annularHighEnergy_column_shells line 519
  30. def OAI.CanonicalQuadraticSieve.coefficientAtScale line 527
  31. theorem OAI.CanonicalQuadraticSieve.coefficientAtScale_shell line 530
  32. theorem OAI.CanonicalQuadraticSieve.coefficientAtScale_row_sum line 538
  33. theorem OAI.CanonicalQuadraticSieve.coefficientAtScale_energy line 568
  34. theorem OAI.CanonicalQuadraticSieve.annularHighEnergy_coefficientAtScale line 597
  35. theorem OAI.CanonicalQuadraticSieve.annularHighEnergy_column_shells_at_scale line 603
  36. theorem OAI.CanonicalQuadraticSieve.dyadicColumnCoefficient_at_scale_energy line 615