OAI/NumberTheory/Ostmann/Quadratic/KernelDiscardBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_large_kernel_discard_bound line 13

   Source documentation

   This is the population estimate used to discard kernels larger than H. The denominator m occurs only through sqrt(m), uniformly over all kernels.

   theorem exists_large_kernel_discard_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (S : Finset ℤ) (f : ℤ → ℤ) (root : ℤ → ℕ)
         (m : ℕ) (h : ℤ) (X H : ℝ), 0 < m → 0 ≤ X → 0 < H →
         h.natAbs.Coprime m →
         (∀ x ∈ S, f x * (root x : ℤ) ^ 2 = (m : ℤ) * x - h) →
         (∀ x ∈ S, ∀ y ∈ S, |((x - y : ℤ) : ℝ)| ≤ X) →
         ((S.filter fun x => H < |(f x : ℝ)|).card : ℝ) ≤
           (S.image f).card * (C * (Real.sqrt (X / H) + Real.sqrt m)) := by
   …