Common reindexing of sifted divisor sums

The polynomial and sieve modulus can vary independently of the divisor tuple set. A congruence witness supplies the discriminant conditions for the split.

noncomputable def NairTenenbaum.PolynomialSystem.siftedDivisorSum {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (T : Finset (Tuple r)) (H : Polynomial ℤ) (M : Tuple r → ℕ) (a b : ℤ) : ℝ

A sifted divisor sum with the divisor set, the sifted polynomial and the modulus as parameters.

Equations

• P.siftedDivisorSum F T H M a b = ∑ m ∈ T, NairTenenbaum.pullback P.exponent F m * ↑(NairTenenbaum.conditionalPolynomialSiftedCount H (M m) P.R m a b)

theorem NairTenenbaum.PolynomialSystem.siftedDivisorSum_le_split {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (T : Finset (Tuple r)) (H : Polynomial ℤ) (M : Tuple r → ℕ) (a b : ℤ) (V : Finset (Tuple r)) (U : Tuple r → Finset (Tuple r)) (hmem : ∀ m ∈ T, ∀ (n : ℤ), (∀ (i : Fin r), ↑(m i) ∣ (Polynomial.eval n (P.R i)).natAbs) → primeReject m P.discriminant.primeFactors ∈ V ∧ primeSelect m P.discriminant.primeFactors ∈ U (primeReject m P.discriminant.primeFactors)) : P.siftedDivisorSum F T H M a b ≤ ∑ v ∈ V, ∑ u ∈ U v, pullback P.exponent F (u * v) * ↑(conditionalPolynomialSiftedCount H (M (u * v)) P.R (u * v) a b)

Generic whole-prime-power split. hmem is the only instance-specific fact.

theorem NairTenenbaum.PolynomialSystem.sum_selected_le_siftedDivisorSum {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (V : Finset (Tuple r)) (H : Polynomial ℤ) (M : Tuple r → ℕ) (a b : ℤ) (T : Finset ℤ) (m : ℤ → Tuple r) (hT : T ⊆ Finset.Ioc a b) (hmap : ∀ t ∈ T, m t ∈ V) (hdiv : ∀ t ∈ T, ∀ (i : Fin r), ↑↑(m t i) ∣ Polynomial.eval t (P.R i)) (hsift : ∀ t ∈ T, (M (m t)).Coprime (Polynomial.eval t H).natAbs) : ∑ t ∈ T, pullback P.exponent F (m t) ≤ P.siftedDivisorSum F V H M a b

Group selected divisor tuples by their fibers; a sieve witness bounds each fiber.