OAI/NumberTheory/JointDickman/Arithmetic/FormRectangleSieve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.formSetWeight line 13
2. theorem OAI.JointDickman.form_rectangle_sieve line 19

   Source documentation

   The rectangular form-weight bound with exact residue averages. Each zero set may be any set of at most p pairs, in particular a proper line.

   theorem form_rectangle_sieve
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {k : ℕ} (hk : 0 < k) :
       ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ)
         (F : ∀ p : P, Fin k → Finset (ZMod p.val × ZMod p.val))
         (θ : P → Fin k → ℝ) (a b c d Z : ℕ), a ≤ b → c ≤ d → 2 ≤ Z →
         (∀ p ∈ P, p.Prime ∧ p ≤ Z ∧ 2 * k ≤ p) →
         (∀ p i, (F p i).card ≤ p.val) → (∀ p i, 0 ≤ θ p i ∧ θ p i ≤ 1) →
         (∑ r ∈ Ico a b, ∑ s ∈ Ico c d, ∏ p : P,
           formSetWeight (F p) (θ p) ((r : ZMod p.val), (s : ZMod p.val))) ≤
         C * ((b : ℝ) - a) * ((d : ℝ) - c) *
           (∏ p : P, (∑ r ∈ range p.val, ∑ s ∈ range p.val,
   …

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