OAI/NumberTheory/Ostmann/Quadratic/KernelPopulationDiscard.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.nat_population_card_le_diameter line 13
2. theorem OAI.Ostmann.kernel_population_card_le line 29
3. theorem OAI.Ostmann.large_kernel_points_card_le line 41

   Source documentation

   There are at most K(D+1) points in the union of the large-kernel fibers, where K is the number of distinct kernels. A subpower common denominator can be retained in D, so no stronger root-count theorem is needed here.

   theorem large_kernel_points_card_le (S : Finset ℤ) (kernel : ℤ → ℤ) (root : ℤ → ℕ)
       (m D : ℕ) (hm : 0 < m) (h : ℤ) (X H : ℝ) (hX : 0 ≤ X) (hH : 0 < H)
       (hroot : ∀ x ∈ S, kernel x * (root x : ℤ) ^ 2 = (m : ℤ) * x - h)
       (hspan : ∀ x ∈ S, ∀ y ∈ S, |((x - y : ℤ) : ℝ)| ≤ X)
       (hD : Real.sqrt ((m : ℝ) * X / H) ≤ D) :
       (S.filter (fun x => H < |(kernel x : ℝ)|)).card ≤ (S.image kernel).card * (D + 1) := by
   …