OAI/NumberTheory/Ostmann/Quadratic/QuadraticSmallMomentMain.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal small-kernel moment: original main term and two corrections

  1. def OAI.Ostmann.quadraticSmallPairCorrection line 13
  2. theorem OAI.Ostmann.quadratic_small_pair_core line 26
  3. def OAI.Ostmann.quadraticSmallMomentCorrections line 36
  4. theorem OAI.Ostmann.quadratic_small_moment_core_decomposition line 42
  5. theorem OAI.Ostmann.quadraticGcdPairs_empty_of_not_odd line 60
  6. theorem OAI.Ostmann.quadratic_small_moment_original_main line 71