OAI/NumberTheory/JointDickman/Arithmetic/AffineRectangleSieve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.affineFormWeight line 11
2. theorem OAI.JointDickman.affine_rectangle_sieve line 17

   Source documentation

   The manuscript's rectangle sieve for proper affine forms, with the exact local mean and an explicit polynomial remainder.

   theorem affine_rectangle_sieve
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {k : ℕ} (hk : 0 < k) :
       ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ)
         (a b c : ∀ p : P, Fin k → ZMod p.val) (θ : P → Fin k → ℝ)
         (u v w x Z : ℕ), u ≤ v → w ≤ x → 2 ≤ Z →
         (∀ p ∈ P, p.Prime ∧ p ≤ Z ∧ 2 * k ≤ p) →
         (∀ p i, a p i ≠ 0 ∨ b p i ≠ 0) →
         (∀ p i, 0 ≤ θ p i ∧ θ p i ≤ 1) →
         (∑ r ∈ Ico u v, ∑ s ∈ Ico w x, ∏ p : P,
           affineFormWeight (a p) (b p) (c p) (θ p) (r : ZMod p.val) (s : ZMod p.val)) ≤
         C * ((v : ℝ) - u) * ((x : ℝ) - w) *
   …

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