OAI/NumberTheory/TwoPoint/Halasz/HalaszMixedCongruenceCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The congruence-counting factor in the complete-system iteration. The jth polynomial sum is fixed only modulo p^min(j,r), and the unused digits are counted before applying the nonsingular full-modulus bound.

  1. theorem OAI.TwoPointCorrelations.halasz_mixed_congruence_count line 12