DyadicPrimeRange.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Concrete dyadic covers of the prime ranges used by the prior comparison

theorem OAI.Ostmann.dyadic_prime_range_cover line 12

Source documentation

A lower endpoint at least twice the modulus ensures every dyadic interval in the cover is long enough for the uniform residue bound.

theorem dyadic_prime_range_cover (A B q : ℕ) (hq : 0 < q) (hA : 2 * q ≤ A)
    (S : Finset ℕ) (hS : ∀ p ∈ S, A ≤ p ∧ p ≤ B) :
    q ≤ 2 ^ Nat.log 2 A ∧
      ∀ p ∈ S, 2 ^ Nat.log 2 A ≤ p ∧ p < 2 ^ (Nat.log 2 A + (Nat.log 2 B + 1)) := by
…

theorem OAI.Ostmann.dyadic_prime_range_count line 28

Source documentation

Even a doubly exponential prime endpoint needs only exponentially many dyadic blocks. The constant is explicit and independent of the tree.

theorem dyadic_prime_range_count (B : ℕ) (C L : ℝ) (hC : 0 ≤ C) (hL : 1 ≤ L)
    (hB : (B : ℝ) ≤ Real.exp (Real.exp (C * L))) :
    ((Nat.log 2 B + 1 : ℕ) : ℝ) ≤
      Real.exp ((C + Real.log ((Real.log 2)⁻¹ + 1)) * L) := by
…