OAI/NumberTheory/TwoPoint/Halasz/HalaszClassicalStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The classical mean-value step using a finite supply of primes. The absolute lower threshold for R comes only from Chebyshev's bounds.

  1. theorem OAI.TwoPointCorrelations.halasz_classical_step line 12