FormIntervalSieve.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Interval sieve for individually weighted forms

Roots may coincide. The Euler factor is the exact residue average of all local form weights, rather than a product that assumes distinct roots.

def OAI.JointDickman.formRootWeight line 17
Source documentation
The product of the weights of all forms vanishing at a residue.
```
noncomputable def formRootWeight {k p : ℕ}
    (root : Fin k → ZMod p) (θ : Fin k → ℝ) (r : ZMod p) : ℝ :=
…
```

theorem OAI.JointDickman.form_interval_sieve line 23

Source documentation

Independently weighting each form gives the precise local residue factor, uniformly even when some roots coincide.

theorem form_interval_sieve
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {k : ℕ} (hk : 0 < k) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset ℕ)
      (root : ∀ p : P, Fin k → ZMod p.val) (θ : P → Fin k → ℝ)
      (a b Z : ℕ), a ≤ b → 2 ≤ Z →
      (∀ p ∈ P, p.Prime ∧ p ≤ Z ∧ 2 * k ≤ p) →
      (∀ p i, 0 ≤ θ p i ∧ θ p i ≤ 1) →
      (∑ n ∈ Ico a b, ∏ p : P, formRootWeight (root p) (θ p) (n : ZMod p.val)) ≤
      C * ((b : ℝ) - a) *
        (∏ p : P, (∑ r ∈ range p.val,
          formRootWeight (root p) (θ p) (r : ZMod p.val)) / p.val) +
…

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