OAI/NumberTheory/TwoPoint/Halasz/HalaszNonsingularMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The nonsingular branch of the classical complete-system iteration. All short-variable residue classes are included.

  1. theorem OAI.TwoPointCorrelations.halasz_fixed_residue_moment line 13
  2. theorem OAI.TwoPointCorrelations.halasz_nonsingular_moment line 44