OAI/NumberTheory/JointDickman/Arithmetic/MixedAffineSieve.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.affine_two_roots_ne line 10
2. theorem OAI.JointDickman.residueWeight_affine line 17
3. theorem OAI.JointDickman.mixed_affine_interval_sieve line 26

   Source documentation

   Negative slopes are included, so the same statement applies when the large numeric addition occurs at either endpoint.

   theorem mixed_affine_interval_sieve
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ (P : Finset ℕ) (a b c d : ℤ) (q : ℝ) (u v Z : ℕ),
         0 ≤ q → q ≤ 1 → u ≤ v → 2 ≤ Z →
         (∀ p ∈ P, p.Prime ∧ p ≤ Z ∧ 4 ≤ p) →
         (∀ p ∈ P, (b : ZMod p) ≠ 0 ∧ (d : ZMod p) ≠ 0 ∧
           (a : ZMod p)*d-c*b ≠ 0) →
         (∑ n ∈ Ico u v, ∏ p ∈ P,
           residueWeight q 0 ((a : ZMod p)+b*n)*residueWeight (1/2) 0 ((c : ZMod p)+d*n)) ≤
           K*((v : ℝ)-u)*(∏ p ∈ P, (1-(3/2-q)/(p : ℝ)))+2*(Z+1 : ℝ)*(Z : ℝ)^2 := by
   …

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