SieveRectangle.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Rectangle sieve with an explicit arithmetic remainder

def OAI.JointDickman.pairRootEvents line 13

theorem OAI.JointDickman.pair_root_sieve_remainder line 18

Source documentation

Actual intersections in a rectangle have the CRT error.

theorem pair_root_sieve_remainder (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (A : ∀ p : ℕ, Finset (ZMod p × ZMod p))
    {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d)
    {D : Finset ℕ} (hD : D ⊆ P) :
    |sieveRemainder
      (fun n : (Ico a b) × (Ico c d) => pairRootEvents P A n.1 n.2)
      (fun _ => 1) (((b : ℝ) - a) * ((d : ℝ) - c))
      (fun p => ((A p).card : ℝ) / (p : ℝ) ^ 2) D| ≤
        2 * ((((b : ℝ) - a) + ((d : ℝ) - c)) / (∏ p ∈ D, (p : ℝ)) + 2) *
          ∏ p ∈ D, ((A p).card : ℝ) := by
…

Mentions: OAI.JointDickman.sieveRemainder, OAI.JointDickman.pairRootEvents

theorem OAI.JointDickman.pair_root_sieve_remainder_le line 54

Source documentation

With at most k*p local residue pairs, the denominator in the CRT error cancels. This includes unions of at most k affine lines.

theorem pair_root_sieve_remainder_le (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (A : ∀ p : ℕ, Finset (ZMod p × ZMod p)) (k : ℕ)
    (hA : ∀ p ∈ P, (A p).card ≤ k * p)
    {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d)
    {D : Finset ℕ} (hD : D ⊆ P) :
    |sieveRemainder
      (fun n : (Ico a b) × (Ico c d) => pairRootEvents P A n.1 n.2)
      (fun _ => 1) (((b : ℝ) - a) * ((d : ℝ) - c))
      (fun p => ((A p).card : ℝ) / (p : ℝ) ^ 2) D| ≤
        2 * (((b : ℝ) - a) + ((d : ℝ) - c) + 2 * ∏ p ∈ D, (p : ℝ)) *
          (k : ℝ) ^ D.card := by
…

Mentions: OAI.JointDickman.sieveRemainder, OAI.JointDickman.pairRootEvents

theorem OAI.JointDickman.sum_rectangle_subtype line 82

theorem OAI.JointDickman.weighted_rectangle_sieve line 93

Source documentation

The weighted rectangle sieve, with all intersection errors evaluated. The only analytic assumptions are the cited Ford and Mertens inputs.

theorem weighted_rectangle_sieve
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {k : ℕ} (hk : 0 < k) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ)
      (A : ∀ p : ℕ, Finset (ZMod p × ZMod p)) (θ : ℕ → ℝ)
      (a b c d Z : ℕ), a ≤ b → c ≤ d → 2 ≤ Z →
      (∀ p ∈ P, p.Prime ∧ p ≤ Z ∧ 2 * k ≤ p) →
      (∀ p ∈ P, (A p).card ≤ k * p) →
      (∀ p ∈ P, 0 ≤ θ p ∧ θ p ≤ 1) →
      (∑ r ∈ Ico a b, ∑ s ∈ Ico c d, ∏ p ∈ pairRootEvents P A r s, θ p) ≤
        C * ((b : ℝ) - a) * ((d : ℝ) - c) *
          (∏ p ∈ P, (1 - ((A p).card : ℝ) / (p : ℝ) ^ 2 +
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.pairRootEvents