OAI/NumberTheory/DirichletL/QuadraticSieve/PoissonConstants.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.list_exists_positive_bound line 80
  2. def OAI.CanonicalQuadraticSieve.poissonPrimitiveConstants line 93
  3. theorem OAI.CanonicalQuadraticSieve.poissonPrimitiveConstants_nonneg line 109
  4. theorem OAI.CanonicalQuadraticSieve.poissonUnitBudget_power_envelope line 138
  5. theorem OAI.CanonicalQuadraticSieve.selectedPoisson_upper line 348
  6. theorem OAI.CanonicalQuadraticSieve.poisson_seven_scale_bounds line 374
  7. theorem OAI.CanonicalQuadraticSieve.power_cutoff_dominates line 422
  8. theorem OAI.CanonicalQuadraticSieve.poisson_truncation_small line 432
  9. theorem OAI.CanonicalQuadraticSieve.poisson_tail_abstract line 448
  10. theorem OAI.CanonicalQuadraticSieve.selectedPoisson_tail_shape line 470
  11. theorem OAI.CanonicalQuadraticSieve.selectedPoisson_principal_shape line 504
  12. def OAI.CanonicalQuadraticSieve.poissonShape line 547
  13. def OAI.CanonicalQuadraticSieve.poissonShapeConstant line 548
  14. theorem OAI.CanonicalQuadraticSieve.poisson_envelope_identity line 550
  15. theorem OAI.CanonicalQuadraticSieve.poissonComparisonMajorant_selected_power line 562