OAI/NumberTheory/DirichletL/QuadraticSieve/MiddleWindows.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.original_middle_window line 98
  2. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.dual_middle_window line 138
  3. theorem OAI.CanonicalQuadraticSieve.large_principal_scale_shape line 184
  4. def OAI.CanonicalQuadraticSieve.principalCorrectionAt line 195
  5. theorem OAI.CanonicalQuadraticSieve.principalCorrectionAt_bound line 216
  6. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.large_principal_correction line 238
  7. theorem OAI.CanonicalQuadraticSieve.sum_two_subtype_pools line 269
  8. theorem OAI.CanonicalQuadraticSieve.originalMiddleWindowAt_eq_finset line 278
  9. theorem OAI.CanonicalQuadraticSieve.originalMiddleWindowAt_dyadic line 298
  10. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.original_middle_pool line 309
  11. theorem OAI.CanonicalQuadraticSieve.dualMiddleWindowAt_eq_finset line 401
  12. theorem OAI.CanonicalQuadraticSieve.dualMiddleWindowAt_dyadic line 421
  13. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.dual_middle_pool line 432
  14. theorem OAI.CanonicalQuadraticSieve.norm_double_sum_real_factor line 521
  15. def OAI.CanonicalQuadraticSieve.originalPrincipalKernel line 530
  16. def OAI.CanonicalQuadraticSieve.originalProductDivisorMiddleAt line 536
  17. theorem OAI.CanonicalQuadraticSieve.originalProductDivisorMiddleAt_nonneg line 545
  18. theorem OAI.CanonicalQuadraticSieve.originalProductDivisorMiddleAt_le_window line 554
  19. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.original_product_divisor_middle line 584