OAI/NumberTheory/Ostmann/Quadratic/QuadraticKernelCollision.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.quadraticSplitPrimes line 12
2. theorem OAI.Ostmann.quadratic_split_avoid line 15
3. theorem OAI.Ostmann.quadratic_kernel_collision_bound line 32

   Source documentation

   No choice of a square root is assumed: Jacobi splitting constructs the rescaling and hence the disjoint residue populations at every retained prime.

   theorem quadratic_kernel_collision_bound (P : Finset ℕ) (S T : Finset ℤ)
       (hSnon : S.Nonempty) (hTnon : T.Nonempty)
       (rootS rootT : ℤ → ℕ) (m Ds Dt : ℕ) (hm : 0 < m)
       (hDs : 1 ≤ Ds) (hDt : 1 ≤ Dt) (h u v : ℤ) (hu : u ≠ 0) (hv : v ≠ 0)
       (hS : ∀ x ∈ S, u * (rootS x : ℤ) ^ 2 = (m : ℤ) * x - h)
       (hT : ∀ y ∈ T, v * (rootT y : ℤ) ^ 2 = (m : ℤ) * y - h)
       (X : ℝ) (hspanS : ∀ x ∈ S, ∀ y ∈ S, |((x - y : ℤ) : ℝ)| ≤ X)
       (hspanT : ∀ x ∈ T, ∀ y ∈ T, |((x - y : ℤ) : ℝ)| ≤ X)
       (hdiamS : Real.sqrt ((m : ℝ) * X / |(u : ℝ)|) ≤ Ds)
       (hdiamT : Real.sqrt ((m : ℝ) * X / |(v : ℝ)|) ≤ Dt)
       (hprimeDiff : ∀ x ∈ S, ∀ y ∈ T, (x - y).natAbs.Prime)
       (L η C : ℝ) (hP : ∀ p ∈ P, p.Prime)
   …