OAI/NumberTheory/JointDickman/Amplification/HyperbolaRounding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Rounding a prime hyperbola to finitely many rectangles

  1. lemma OAI.JointDickman.interval_sum_difference_norm line 9
  2. lemma OAI.JointDickman.rounded_cutoff_le line 20
  3. lemma OAI.JointDickman.rounded_cutoff_error line 24
  4. lemma OAI.JointDickman.rounded_hyperbola_error line 33
  5. lemma OAI.JointDickman.rounded_hyperbola_rectangles line 54
  6. lemma OAI.JointDickman.quotient_cell_count line 72
  7. lemma OAI.JointDickman.quotient_cell_width line 79

    Source documentation

    The grid width is at most its real target plus one.

    lemma quotient_cell_width (M H : ℕ) (hH : 0 < H) :
    ((M/H+1:ℕ):ℝ) ≤ (M:ℝ)/H+1 := by
…