OAI/NumberTheory/Ostmann/QuadraticCenter/ExceptionalKernelFamilyBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.kernel_sqrt_quotient_bound line 10
2. theorem OAI.Ostmann.exists_exceptional_kernel_family_bound line 32

   Source documentation

   At most 32 possible signed products are lost. The conductor lower bound replaces each product size in the previously proved population estimate.

   theorem exists_exceptional_kernel_family_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (S T : Finset ℤ) (f g : ℤ → ℤ)
         (r s : ℤ → ℕ) (m q : ℕ) (h : ℤ) (X : ℝ),
         0 < m → 0 < q → 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 ∈ largeConductorKernelCandidates q).card : ℝ) ≤
   …

   Mentions: OAI.Ostmann.largeConductorKernelCandidates