OAI/NumberTheory/TwoPoint/Halasz/HalaszZeroRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The zero-representation inequality used for the translated complete systems: any prescribed difference has at most as many representations as zero. This is Proposition ZRD in Ford's mean-value argument.

  1. def OAI.TwoPointCorrelations.halaszRepresentationCount line 13
  2. def OAI.TwoPointCorrelations.halaszRepresentationSum line 18
  3. def OAI.TwoPointCorrelations.halaszRepresentationWeight line 22
  4. theorem OAI.TwoPointCorrelations.halasz_representation_integral line 27
  5. lemma OAI.TwoPointCorrelations.halasz_representation_weight_norm line 46
  6. lemma OAI.TwoPointCorrelations.halasz_representation_energy line 52
  7. theorem OAI.TwoPointCorrelations.halasz_zero_representation_dominates line 64