OAI/NumberTheory/DirichletL/QuadraticSieve/PrincipalMajorants.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.smallPrincipalMajorant line 84
  2. lemma OAI.CanonicalQuadraticSieve.smallPrincipalMajorant_nonneg line 91
  3. lemma OAI.CanonicalQuadraticSieve.smallPrincipalMajorant_mono line 101
  4. def OAI.CanonicalQuadraticSieve.unrestrictedSmallPrincipalSum line 120
  5. lemma OAI.CanonicalQuadraticSieve.unrestrictedSmallPrincipalSum_sector line 130
  6. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.small_principal_sector line 150
  7. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.unrestricted_small_principal_sum line 227
  8. theorem OAI.CanonicalQuadraticSieve.weightedDivisorCorrection_coprime_mask line 270
  9. def OAI.CanonicalQuadraticSieve.maskedPrincipalDivisorCorrection line 307
  10. theorem OAI.CanonicalQuadraticSieve.maskedPrincipalDivisorCorrection_eq line 317
  11. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.masked_source_large_principal_sum line 361
  12. lemma OAI.CanonicalQuadraticSieve.smallPrincipalMajorant_bad_scale line 418
  13. lemma OAI.CanonicalQuadraticSieve.sqrt_sector_scale line 441
  14. def OAI.CanonicalQuadraticSieve.unrestrictedLargePrincipalSum line 451
  15. lemma OAI.CanonicalQuadraticSieve.unrestrictedLargePrincipalSum_sector line 461
  16. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.large_principal_sector line 501
  17. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.unrestricted_large_principal_sum line 589
  18. lemma OAI.CanonicalQuadraticSieve.unrestrictedPairTerm_norm_le line 632
  19. theorem OAI.CanonicalQuadraticSieve.unrestricted_pair_error_energy line 648
  20. theorem OAI.CanonicalQuadraticSieve.unrestricted_pair_error_ideal_bound line 686
  21. def OAI.CanonicalQuadraticSieve.unrestrictedDualPrincipalErrorSum line 703
  22. theorem OAI.CanonicalQuadraticSieve.unrestrictedDualPrincipal_actual_error_sum_bound line 714