Selected smooth prefixes at prime arguments with a lower mass cutoff #
theorem
NairTenenbaum.PolynomialSystem.sum_selectedPrimeSmoothTailDivisors_le
{k r : ℕ}
(P : PolynomialSystem k r)
{F : ArithmeticMap k}
(hF : ∀ (n : Tuple k), 0 ≤ F n)
(g : ℕ)
(N : ℕ+)
(s : Finset ℕ)
(X : ℝ)
(a b : ℤ)
(z : ℝ)
(T : Finset ℤ)
(m : ℤ → Tuple r)
(hT : T ⊆ Finset.Ioc a b)
(hz : 0 ≤ z)
(htPrime : ∀ t ∈ T, Nat.Prime t.natAbs)
(htLarge : ∀ t ∈ T, z < ↑t.natAbs)
(hm : ∀ t ∈ T, weightedMass P.exponent (m t) ≤ ↑N)
(hdiv : ∀ t ∈ T, ∀ (i : Fin r), ↑↑(m t i) ∣ Polynomial.eval t (P.R i))
(hsmooth : ∀ t ∈ T, ∀ (i : Fin r), ↑(m t i) ∈ Nat.factoredNumbers s)
(hlarge : ∀ t ∈ T, X < ↑(weightedMass P.exponent (m t)))
(hsift : ∀ t ∈ T, (sieveModulus P.total (mass (m t)) z).Coprime (Polynomial.eval t P.total).natAbs)
:
Grouping selected divisors preserves both smoothness and the lower mass cutoff. Distinct integers can have the same selected tuple.
theorem
NairTenenbaum.PolynomialSystem.sum_primeRoughSmoothTailPrefix_le
{k r : ℕ}
(P : PolynomialSystem k r)
{A B σ : ℝ}
{F : ArithmeticMap k}
(hF : Admissible A B σ F)
(hA : 1 ≤ A)
(hB : 0 ≤ B)
(g : ℕ)
(N : ℕ+)
(s : Finset ℕ)
(X : ℝ)
(a b : ℤ)
(T : Finset ℤ)
(n : ℤ → Tuple r)
(q : ℤ → ℕ)
(hT : T ⊆ Finset.Ioc a b)
(hn : ∀ t ∈ T, ∀ (i : Fin r), ↑(n t i) = (Polynomial.eval t (P.R i)).natAbs)
{x α c : ℝ}
(hx : 1 < x)
(hα : 0 < α)
(htPrime : ∀ t ∈ T, Nat.Prime t.natAbs)
(htLarge : ∀ t ∈ T, x ^ α < ↑t.natAbs)
(hq : ∀ t ∈ T, x ^ α < ↑(q t))
(hsmall : ∀ t ∈ T, weightedMass P.exponent (primeSelect (n t) (Finset.range (q t))) ≤ ↑N)
(hsmooth : ∀ t ∈ T, ∀ (i : Fin r), ↑(primeSelect (n t) (Finset.range (q t)) i) ∈ Nat.factoredNumbers s)
(hlarge : ∀ t ∈ T, X < ↑(weightedMass P.exponent (primeSelect (n t) (Finset.range (q t)))))
(hvalue : ∀ t ∈ T, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c)
:
(∑ t ∈ T, extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs) ≤ A ^ (c / α) * P.primeSmoothTailSiftedSum F g N s X a b (x ^ α)
Rough remainders can be removed while retaining the smooth mass tail of
the selected prefix. The sifting cutoff is x^α; its relation to the smoothness
support is unrestricted.