OAI/NumberTheory/Ostmann/QuadraticSieve/PublishedQuadraticSieve.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The published quadratic large-sieve input

D. R. Heath-Brown, A mean value estimate for real character sums, Acta Arithmetica 72 (1995), 235–275, Theorem 1, DOI 10.4064/aa-72-3-235-275.

Only the finite odd-squarefree coefficient inequality is retained. The symbol is Mathlib's Jacobi symbol.

  1. def OAI.Ostmann.oddSquarefreeRange line 20
  2. def OAI.Ostmann.quadraticSieveSum line 23
  3. def OAI.Ostmann.quadraticSieveEnergy line 26
  4. def OAI.Ostmann.PublishedQuadraticLargeSieve line 31

    Source documentation

    Heath-Brown's Theorem 1, specialized to integer bounds and finite coefficient arrays. This is an explicit hypothesis, not a global axiom.

    def PublishedQuadraticLargeSieve : Prop :=
…