OAI/NumberTheory/Ostmann/Construction/EndpointKernelPairCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.endpoint_kernel_product_count line 13
2. theorem OAI.Ostmann.exists_endpoint_kernel_product_bound line 52

   Source documentation

   The exceptional signed product accounts for few endpoint pairs. The bound is uniform over the two finite endpoint sets and their affine square roots.

   theorem exists_endpoint_kernel_product_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (S T : Finset ℤ) (f g : ℤ → ℤ)
         (r s : ℤ → ℕ) (m : ℕ) (h d : ℤ) (X : ℝ),
         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) →
         (Fintype.card {z : S × T // f z.1 * g z.2 = d} : ℝ) ≤
   …