OAI/NumberTheory/Ostmann/Preliminaries/MultiplicativeSieveProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite multiplicative large sieve for the complex-zero density argument

Summing the full character Parseval identity before discarding imprimitive characters retains the conductor saving in the Gauss normalization.

  1. theorem OAI.Ostmann.primitive_multiplicative_large_sieve line 16