OAI/NumberTheory/Ostmann/ZeroDensity/DensityHybridSieve.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A hybrid large sieve with an absolute constant

The character and height variables are averaged simultaneously. The proof uses short logarithmic windows and the already proved finite additive large sieve.

  1. theorem OAI.Ostmann.hybrid_multiplicative_large_sieve line 16