MixedTwoFormSieve.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The two-form sieve with a Rankin weight and a half weight

theorem OAI.JointDickman.formRootWeight_two_mixed line 10
theorem OAI.JointDickman.mixed_two_root_mean line 19

theorem OAI.JointDickman.mixed_two_root_interval_sieve line 29

Source documentation

Only the two weights needed by the numeric-addition argument are used. The product is the exact local density for distinct roots.

theorem mixed_two_root_interval_sieve
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ (P : Finset ℕ)
      (a b : (p : P) → ZMod p.val) (q : ℝ) (u v Z : ℕ),
      0 ≤ q → q ≤ 1 → u ≤ v → 2 ≤ Z →
      (∀ p ∈ P, p.Prime ∧ p ≤ Z ∧ 4 ≤ p) → (∀ p, a p ≠ b p) →
      (∑ n ∈ Ico u v, ∏ p : P,
        residueWeight q (a p) (n : ZMod p.val)*residueWeight (1/2) (b p) (n : ZMod p.val)) ≤
        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