OAI/NumberTheory/Ostmann/Quadratic/RootPopulationBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A concrete diameter and collision budget for large root populations

  1. def OAI.Ostmann.naturalRootDiameter line 12
  2. theorem OAI.Ostmann.naturalRootDiameter_bounds line 15
  3. theorem OAI.Ostmann.naturalRootDiameter_dominates line 40
  4. theorem OAI.Ostmann.root_population_collision_budget line 52

    Source documentation

    Cardinalities at least Q make the two sampling losses at most 2 log 4. The diameter loss then leaves the manuscript's 1.01L budget.

    theorem root_population_collision_budget (m Q a b : ℕ) (L η : ℝ)
    (hm : 0 < m) (hQ : 0 < Q) (hL : 1000 ≤ L) (hη : η ≤ 1 / 1000)
    (hmupper : (m : ℝ) ≤ Real.exp (η * L)) (ha : Q ≤ a) (hb : Q ≤ b) :
    2 * Real.log (naturalRootDiameter m L : ℝ) +
      (1 / (a : ℝ) + 1 / (b : ℝ)) * ∑ p ∈ Nat.primesLE Q, Real.log (p : ℝ) ≤
        (101 / 100 : ℝ) * L := by
…

    Mentions: OAI.Ostmann.naturalRootDiameter