OAI/NumberTheory/Ostmann/Quadratic/QuadraticMomentMainComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual two transformed main terms, summed over the original pairs

  1. def OAI.Ostmann.quadraticSmallPairMain line 14
  2. def OAI.Ostmann.quadraticPairMainDifference line 19
  3. theorem OAI.Ostmann.quadratic_small_pair_core_main line 22
  4. theorem OAI.Ostmann.quadratic_pair_main_difference_sum line 33
  5. theorem OAI.Ostmann.quadraticGcdPairs_empty_of_not_squarefree line 49
  6. def OAI.Ostmann.quadraticMomentMainDifference line 60
  7. def OAI.Ostmann.quadraticMainComparisonCost line 63
  8. theorem OAI.Ostmann.quadratic_moment_main_comparison line 66
  9. theorem OAI.Ostmann.quadratic_off_diagonal_main_comparison line 103