OAI/NumberTheory/Ostmann/Quadratic/KernelPopulationBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The congruence-refined population bound for a fixed signed kernel

  1. theorem OAI.Ostmann.kernel_population_residue_bound line 13
  2. theorem OAI.Ostmann.kernel_population_real_bound line 28
  3. theorem OAI.Ostmann.sqrt_modulus_cancel line 48
  4. theorem OAI.Ostmann.exists_kernel_population_uniform_bound line 58

    Source documentation

    The denominator loss is absorbed into an absolute constant. The remaining sqrt(m) term is subpower for the common centers constructed in the application.

    theorem exists_kernel_population_uniform_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : Finset ℤ) (root : ℤ → ℕ) (m : ℕ) (h u : ℤ) (X : ℝ),
      0 < m → u ≠ 0 → h.natAbs.Coprime m →
      (∀ x ∈ S, u * (root x : ℤ) ^ 2 = (m : ℤ) * x - h) →
      (∀ x ∈ S, ∀ y ∈ S, |((x - y : ℤ) : ℝ)| ≤ X) →
      (S.card : ℝ) ≤ C * (Real.sqrt (X / |(u : ℝ)|) + Real.sqrt m) := by
…