OAI/NumberTheory/DirichletL/QuadraticSieve/RetainedDualBounds.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.primePoolDensity line 83
  2. theorem OAI.CanonicalQuadraticSieve.principalTruncation_scaled line 86
  3. def OAI.CanonicalQuadraticSieve.unrestrictedPrincipalDensity line 122
  4. def OAI.CanonicalQuadraticSieve.unrestrictedDualPrincipalTruncation line 128
  5. theorem OAI.CanonicalQuadraticSieve.unrestrictedDualPrincipalTruncation_eq line 138
  6. theorem OAI.CanonicalQuadraticSieve.dualPrincipalIdeal_truncated_all_conductors line 186
  7. theorem OAI.CanonicalQuadraticSieve.unrestrictedDualPrincipal_error_uniform line 239
  8. def OAI.CanonicalQuadraticSieve.retainedDualPrincipalSum line 297
  9. theorem OAI.CanonicalQuadraticSieve.retainedDualPrincipalSum_symmetric_truncation line 306
  10. lemma OAI.CanonicalQuadraticSieve.norm_four_correction_terms line 338
  11. theorem OAI.CanonicalQuadraticSieve.retained_dual_principal_difference line 346
  12. lemma OAI.CanonicalQuadraticSieve.sum_ideal_subtype_dyadic line 404
  13. def OAI.CanonicalQuadraticSieve.retainedDualMajorant line 412
  14. lemma OAI.CanonicalQuadraticSieve.retainedDualMajorant_nonneg line 422
  15. lemma OAI.CanonicalQuadraticSieve.retainedDualMajorant_mono line 435
  16. lemma OAI.CanonicalQuadraticSieve.retainedDualPrincipalDifference_dyadic line 452
  17. theorem OAI.CanonicalQuadraticSieve.retained_dual_principal_global line 467
  18. def OAI.CanonicalQuadraticSieve.highSquareParts line 531
  19. theorem OAI.CanonicalQuadraticSieve.highSquareParts_bounds line 533
  20. theorem OAI.CanonicalQuadraticSieve.highSquarePart_fiber_row_bounds line 559
  21. def OAI.CanonicalQuadraticSieve.highSquarePartFiber line 574
  22. theorem OAI.CanonicalQuadraticSieve.highSquarePartFiber_energy line 577
  23. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_le_squarePart_sum line 630