SignedQuadraticSieve.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The signed kernel form follows from Heath-Brown's published theorem

def OAI.Ostmann.quadraticNumeratorTwist line 12
theorem OAI.Ostmann.quadraticSieveEnergy_numeratorTwist_le line 15
theorem OAI.Ostmann.quadraticTransposeSum_mul line 22
theorem OAI.Ostmann.quadratic_twist_sum_bound line 29
theorem OAI.Ostmann.quadratic_signed_bound line 47
Source documentation
Four numerator twists and two reciprocity classes suffice, including the kernels 1 and -1. The constant here is exactly eight times the published one.
```
theorem quadratic_signed_bound (P : PublishedQuadraticLargeSieve)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ M N : ℕ, 1 ≤ M → 1 ≤ N → ∀ b : ℕ → ℂ,
      (∑ u ∈ signedSquarefreeRange M, ‖quadraticTransposeSum N b u‖ ^ 2) ≤
        C * ((M : ℝ) * N) ^ ε * ((M : ℝ) + N) * quadraticSieveEnergy N b := by
…
```
Mentions: OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.signedSquarefreeRange, OAI.Ostmann.quadraticTransposeSum, OAI.Ostmann.quadraticSieveEnergy

theorem OAI.Ostmann.quadratic_kernel_count line 73

Source documentation

The genuine finite kernel-count consequence. Its sole analytic hypothesis is the published large sieve, and the test array is shared by all kernels.

theorem quadratic_kernel_count (P : PublishedQuadraticLargeSieve)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (M N : ℕ) (b : ℕ → ℂ) (U : Finset ℤ) (a : ℝ),
      1 ≤ M → 1 ≤ N → 0 < a → U ⊆ signedSquarefreeRange M →
      (∀ u ∈ U, a ≤ ‖quadraticTransposeSum N b u‖) →
      (U.card : ℝ) ≤ C * ((M : ℝ) * N) ^ ε * ((M : ℝ) + N) *
        quadraticSieveEnergy N b / a ^ 2 := by
…

Mentions: OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.signedSquarefreeRange, OAI.Ostmann.quadraticTransposeSum, OAI.Ostmann.quadraticSieveEnergy