OAI/NumberTheory/Ostmann/Quadratic/QuadraticGaussBilinear.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Separating the Gauss factor in the actual divisor bilinear sum

  1. def OAI.Ostmann.quadraticGaussLeft line 12
  2. def OAI.Ostmann.quadraticGaussRight line 15
  3. def OAI.Ostmann.quadraticThreeClass line 18
  4. def OAI.Ostmann.quadraticGaussDivisorBilinear line 21
  5. theorem OAI.Ostmann.quadratic_gauss_divisor_bilinear_split line 28
  6. theorem OAI.Ostmann.quadraticGaussLeft_norm line 53
  7. theorem OAI.Ostmann.quadraticGaussRight_norm line 58
  8. theorem OAI.Ostmann.quadraticSieveEnergy_gaussLeft line 64
  9. theorem OAI.Ostmann.quadraticSieveEnergy_gaussRight line 70
  10. theorem OAI.Ostmann.quadraticSieveEnergy_threeClass line 76
  11. theorem OAI.Ostmann.quadraticDivisorMoment_gaussLeft line 85
  12. theorem OAI.Ostmann.quadraticDivisorMoment_gaussRight line 91
  13. theorem OAI.Ostmann.quadraticDivisorMoment_threeClass line 97