QuadraticKernelCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative kernel counting from a shared character bias

theorem OAI.Ostmann.quadratic_biased_kernel_count line 15

Source documentation

Heath-Brown's quadratic large sieve bounds the number of signed squarefree kernels with a common amplified character bias.

theorem quadratic_biased_kernel_count (sieve : PublishedQuadraticLargeSieve)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ) (k Z M : ℕ) (e : ℕ → ℂ)
      (U : Finset ℤ) (c : ℝ),
      (∀ p ∈ P, p.Prime) → (∀ p ∈ P, Odd p) → (∀ p ∈ P, p ≤ Z) →
      (∀ p ∈ P, ‖e p‖ ≤ 1) → 0 < P.card → 1 ≤ k → 1 ≤ Z → 1 ≤ M →
      0 ≤ c → 0 < c ^ k - (k : ℝ) ^ 2 / P.card →
      U ⊆ signedSquarefreeRange M →
      (∀ u ∈ U, c ≤ ‖quadraticPrimeMean P e u‖) →
      (U.card : ℝ) ≤ C * ((M : ℝ) * Z ^ k) ^ ε * ((M : ℝ) + Z ^ k) *
        ((k.factorial : ℝ) / (P.card : ℝ) ^ k) /
          (c ^ k - (k : ℝ) ^ 2 / P.card) ^ 2 := by
…

Mentions: OAI.Ostmann.PublishedQuadraticLargeSieve, OAI.Ostmann.signedSquarefreeRange, OAI.Ostmann.quadraticPrimeMean

theorem OAI.Ostmann.affine_kernel_image_subset line 45

Source documentation

The squarefree kernels of the affine values lie in the range determined by the interval, denominator and numerator.

theorem affine_kernel_image_subset (S : Finset ℤ) (X m : ℕ) (h : ℤ)
    (kernel : ℤ → ℤ) (root : ℤ → ℕ)
    (hX : ∀ x ∈ S, |x| ≤ X)
    (hkernel : ∀ x ∈ S, kernel x ≠ 0 ∧ 0 < root x ∧ Squarefree (kernel x).natAbs ∧
      kernel x * (root x : ℤ) ^ 2 = (m : ℤ) * x - h) :
    S.image kernel ⊆ signedSquarefreeRange (m * X + h.natAbs) := by
…

Mentions: OAI.Ostmann.signedSquarefreeRange