OAI/NumberTheory/TwoPoint/Halasz/HalaszClassicalDefect.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The geometric defect in the classical Vinogradov iteration.

  1. def OAI.TwoPointCorrelations.halaszTriangularDegree line 8
  2. def OAI.TwoPointCorrelations.halaszTotalDegree line 10
  3. def OAI.TwoPointCorrelations.halaszClassicalDefect line 12
  4. def OAI.TwoPointCorrelations.halaszClassicalExponent line 15
  5. lemma OAI.TwoPointCorrelations.halasz_triangular_degree_cast line 18
  6. lemma OAI.TwoPointCorrelations.halasz_total_degree_cast line 26
  7. lemma OAI.TwoPointCorrelations.halasz_classical_ratio_bounds line 31
  8. lemma OAI.TwoPointCorrelations.halasz_classical_defect_bounds line 38
  9. lemma OAI.TwoPointCorrelations.halasz_classical_defect_successor line 47
  10. lemma OAI.TwoPointCorrelations.halasz_classical_exponent_zero line 52
  11. lemma OAI.TwoPointCorrelations.halasz_classical_exponent_successor line 57
  12. lemma OAI.TwoPointCorrelations.halasz_classical_exponent_bounds line 64
  13. lemma OAI.TwoPointCorrelations.halasz_classical_exponent_normalization line 86