OAI/NumberTheory/Ostmann/QuadraticCenter/PageKernelPopulation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_page_kernel_population_bound line 11

   Source documentation

   The threshold R replaces the actual exceptional conductor uniformly. At R=(log X)^100 the leading cost is X/(log X)^50.

   theorem exists_page_kernel_population_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (P : PublishedProgressionInput) (Q₀ : ℕ) (R : ℝ)
         (S T : Finset ℤ) (f g : ℤ → ℤ) (r s : ℤ → ℕ) (m : ℕ) (h : ℤ) (X : ℝ),
         0 < R → 0 < m → 0 ≤ X →
         (∀ x ∈ S, f x ≠ 0) → (∀ y ∈ T, g y ≠ 0) →
         h.natAbs.Coprime m →
         (∀ x ∈ S, f x * (r x : ℤ) ^ 2 = (m : ℤ) * x - h) →
         (∀ y ∈ T, g y * (s y : ℤ) ^ 2 = (m : ℤ) * y - h) →
         (∀ x ∈ S, ∀ y ∈ S, |((x - y : ℤ) : ℝ)| ≤ X) →
         (∀ x ∈ T, ∀ y ∈ T, |((x - y : ℤ) : ℝ)| ≤ X) →
         (∀ x ∈ S, ∀ y ∈ T, (f x).natAbs.Coprime (g y).natAbs) →
         (((S.product T).filter fun z => f z.1 * g z.2 ∈ pageKernelExclusion P Q₀ R).card : ℝ) ≤
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.pageKernelExclusion