OAI/NumberTheory/Ostmann/QuadraticSieveDualCorrelationsParts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.QuadraticSieve.dualCorrelationFiniteForm line 9
  2. def OAI.Ostmann.QuadraticSieve.dualSquareLeading line 14
  3. def OAI.Ostmann.QuadraticSieve.dualSquareZeroCorrection line 18
  4. def OAI.Ostmann.QuadraticSieve.dualSquareLargeCorrection line 22
  5. def OAI.Ostmann.QuadraticSieve.dualSquareFourierCorrection line 28
  6. def OAI.Ostmann.QuadraticSieve.dualCorrelationLeadingTerm line 35
  7. def OAI.Ostmann.QuadraticSieve.dualCorrelationZeroTerm line 38
  8. def OAI.Ostmann.QuadraticSieve.dualCorrelationLargeTerm line 42
  9. def OAI.Ostmann.QuadraticSieve.dualCorrelationFourierTerm line 46
  10. theorem OAI.Ostmann.QuadraticSieve.dualCorrelationMainTerm_parts line 51
  11. theorem OAI.Ostmann.QuadraticSieve.dualCorrelationLeadingTerm_eq line 69