OAI/NumberTheory/DirichletL/QuadraticSieve/MaskedPrincipalBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.middleTruncation_coprime_common_mask line 80
  2. theorem OAI.CanonicalQuadraticSieve.sqrt_norm_divisor_scale line 133
  3. def OAI.CanonicalQuadraticSieve.originalMaskedTruncatedMiddle line 141
  4. theorem OAI.CanonicalQuadraticSieve.originalMaskedTruncatedMiddle_eq_divisors line 149
  5. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.original_masked_truncated_middle line 190
  6. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.actual_principal_difference line 256
  7. theorem OAI.ShortDraftDescent.integral_geometric_descent line 297
  8. def OAI.CanonicalQuadraticSieve.halfShellFactor line 346
  9. lemma OAI.CanonicalQuadraticSieve.halfShellFactor_nonneg line 348
  10. lemma OAI.CanonicalQuadraticSieve.halfShellFactor_le_one line 352
  11. lemma OAI.CanonicalQuadraticSieve.halfShellFactor_pair line 357
  12. def OAI.CanonicalQuadraticSieve.smallPrincipalCorrection line 373
  13. lemma OAI.CanonicalQuadraticSieve.originalTerm_real_scaling line 381
  14. theorem OAI.CanonicalQuadraticSieve.smallPrincipalCorrection_bound line 393
  15. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.small_principal_correction line 452
  16. theorem OAI.CanonicalQuadraticSieve.truncationError_symmetric_bound line 487
  17. theorem OAI.CanonicalQuadraticSieve.primePool_symmetric_error_bound line 508
  18. theorem OAI.CanonicalQuadraticSieve.lowPrincipal_symmetric_error_bound line 527
  19. theorem OAI.CanonicalQuadraticSieve.originalTerm_one_norm_le line 555
  20. theorem OAI.CanonicalQuadraticSieve.actual_pair_error_energy line 573
  21. theorem OAI.CanonicalQuadraticSieve.finite_ideal_family_card_bound line 611
  22. theorem OAI.CanonicalQuadraticSieve.actual_pair_error_ideal_bound line 621