Uniform smooth moments before taking the tail #
Keeping the positive moment explicit allows it to be combined with the moment of the full bad-prime part before applying the mass-tail inequality.
theorem
NairTenenbaum.totient_weight_smooth_moment_finite
{k r : ℕ}
{A B ε κ z : ℝ}
{F : ArithmeticMap k}
(hF : Admissible A B ε F)
(hA : 0 ≤ A)
(hB : 1 ≤ B)
(hε : 0 < ε)
(hκ : 0 ≤ κ)
(hz : 2 ≤ z)
(γ : Fin k → Fin r → ℕ)
(hγ : ∀ (i : Fin r), 0 < totalExponent γ i)
(hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε ≤ 1 / 8)
(Q : Fin r → Polynomial ℤ)
(C : Fin r → ℕ)
(hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i)
(G : ℕ)
(hG : ∀ (i : Fin r), totalExponent γ i ≤ G)
(hzκ : 4 ^ (↑G * κ) ≤ z)
(g D : ℕ)
(N : ℕ+)
:
∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N,
(rootTupleWeight γ F Q n * ∏ i : Fin r, totientTwist g ↑(n i)) * ↑(weightedMass γ n) ^ (κ / Real.log z) ≤ totientSmoothTailBound A B κ γ C G g * ∑ m ∈ positiveUpTo z, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m
theorem
NairTenenbaum.PolynomialSystem.totient_smooth_moment_uniform
{k r : ℕ}
(P : PolynomialSystem k r)
{A B ε κ z : ℝ}
{F : ArithmeticMap k}
(hF : Admissible A B ε F)
(hA : 0 ≤ A)
(hB : 1 ≤ B)
(hε : 0 < ε)
(hκ : 0 ≤ κ)
(hz : 2 ≤ z)
(hzκ : 4 ^ (↑P.total.natDegree * κ) ≤ z)
(hgε : ↑P.total.natDegree * ε ≤ 1 / 8)
(N : ℕ+)
:
∑ n ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N,
(rootTupleWeight P.exponent F P.R n * ∏ i : Fin r, totientTwist P.total.natDegree ↑(n i)) * ↑(weightedMass P.exponent n) ^ (κ / Real.log z) ≤ smoothTailUniformBound A B κ P.total.natDegree P.badDiscriminant * ∑ m ∈ positiveUpTo z, P.weight F m
Coefficient-uniform smooth moment for the totient-modified weight.