OAI/NumberTheory/DirichletL/QuadraticSieve/DyadicColumns.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.columnDyadicLength line 76
  2. theorem OAI.CanonicalQuadraticSieve.columnDyadicLength_cover line 78
  3. theorem OAI.CanonicalQuadraticSieve.columnDyadicLength_small_power line 83
  4. theorem OAI.CanonicalQuadraticSieve.annularHighEnergy_column_shells_small_power line 99
  5. theorem OAI.CanonicalQuadraticSieve.squarefreePart_norm_le line 117
  6. def OAI.CanonicalQuadraticSieve.dualSquarefreeTail line 124
  7. theorem OAI.CanonicalQuadraticSieve.dualSquarefreeTail_bound line 128
  8. def OAI.CubicEisenstein.fullIdealWeight line 189
  9. lemma OAI.CubicEisenstein.fullIdealWeight_good line 192
  10. lemma OAI.CubicEisenstein.norm_fullIdealWeight line 195
  11. theorem OAI.CubicEisenstein.fullIdealWeight_summable_norm line 209
  12. def OAI.CubicEisenstein.fullIdealZeta line 226
  13. lemma OAI.CubicEisenstein.fullIdealWeight_norm_fiber line 228
  14. theorem OAI.CubicEisenstein.fullIdealZeta_eq_dedekindZeta line 245
  15. lemma OAI.CubicEisenstein.fullIdealWeight_lambdaFactor line 253
  16. theorem OAI.CubicEisenstein.unramifiedIdealZeta_eq_dedekindZeta line 264
  17. lemma OAI.CubicEisenstein.constantDirichletTerm_differentiable line 314
  18. lemma OAI.CubicEisenstein.constantDirichletTerm_norm_mono line 324
  19. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_zero_differentiableAt line 339
  20. lemma OAI.CubicEisenstein.unramifiedNormWeight_differentiable line 353
  21. lemma OAI.CubicEisenstein.unramifiedNormWeight_norm_mono line 363
  22. theorem OAI.CubicEisenstein.unramifiedIdealZeta_differentiableAt line 376
  23. def OAI.CubicEisenstein.unramifiedZetaResidue line 397
  24. lemma OAI.CubicEisenstein.unramifiedZetaResidue_ne_zero line 400
  25. theorem OAI.CubicEisenstein.unramifiedIdealZeta_oneSidedResidue line 405
  26. lemma OAI.CubicEisenstein.cusp_volume_ne_zero line 423
  27. def OAI.CubicEisenstein.constantArithmeticResidue line 427
  28. lemma OAI.CubicEisenstein.constantArithmeticResidue_ne_zero line 430
  29. lemma OAI.CubicEisenstein.tendsto_three_mul_sub_three_four_thirds line 435
  30. theorem OAI.CubicEisenstein.scatteringCoefficient_zero_oneSidedResidue line 445
  31. theorem OAI.CanonicalQuadraticSieve.idealQuotient_in_shell line 491
  32. theorem OAI.CanonicalQuadraticSieve.residual_modulus_norm_shell line 506
  33. theorem OAI.CanonicalQuadraticSieve.residual_poisson_prefactor_le line 538
  34. def OAI.CanonicalQuadraticSieve.dualSquarefreeLow line 558
  35. theorem OAI.CanonicalQuadraticSieve.dual_ideal_low_add_tail line 562
  36. theorem OAI.CanonicalQuadraticSieve.dualSquarefreeLow_principal line 596