OAI/NumberTheory/JointDickman/Arithmetic/ThreeFormSieve.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.real_residue_sum_eq_range line 12
2. theorem OAI.JointDickman.real_residue_double_sum_eq_range line 17
3. def OAI.JointDickman.threeFormLocalFactor line 26
4. theorem OAI.JointDickman.threeFormLocalFactor_eq_mean line 31
5. theorem OAI.JointDickman.threeFormLocalFactor_nonneg line 36
6. theorem OAI.JointDickman.three_form_local_product_bound line 44
7. def OAI.JointDickman.threeFormSieveWeight line 79
8. theorem OAI.JointDickman.three_form_rectangle_sieve line 85

   Source documentation

   The actual three-form sieve, with a separated singular factor and an explicit polynomial remainder.

   theorem three_form_rectangle_sieve
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ) (θ : ℕ → ℝ)
         (j u v w x Z : ℕ), j ≠ 0 → u ≤ v → w ≤ x → 2 ≤ Z →
         (∀ p ∈ P, p.Prime ∧ p ≤ Z ∧ 6 ≤ p) →
         (∀ p ∈ P, 0 ≤ θ p ∧ θ p ≤ 1) →
         (∑ b ∈ Ico u v, ∑ c ∈ Ico w x, threeFormSieveWeight P θ j b c) ≤
           C * ((v : ℝ) - u) * ((x : ℝ) - w) *
             (∏ p ∈ P, (1 - (1 - θ p) / p)) ^ 3 * singularFactor 24 j +
           2 * (((v : ℝ) - u) + ((x : ℝ) - w) + 2 * Z) * (Z + 1 : ℝ) * (Z : ℝ) ^ 3 := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.threeFormSieveWeight, OAI.JointDickman.singularFactor