OAI/NumberTheory/TwoPoint/Halasz/HalaszCollisionMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The analytic estimate for a repeated coordinate in a Vinogradov system. The scaled polynomial records the repeated variable exactly.

  1. lemma OAI.TwoPointCorrelations.halasz_torus_cauchy line 12
  2. lemma OAI.TwoPointCorrelations.halasz_collision_interpoland line 29
  3. def OAI.TwoPointCorrelations.halaszCollisionMoment line 47
  4. theorem OAI.TwoPointCorrelations.halasz_collision_moment_bound line 51