The smooth tail estimate for the root vector

The moment bound, prime-band comparison, and absorption argument give the root-vector specialization of Lemma 2. The infinite tail is a proved convergent series. The totient-modified root vector is treated separately in TotientSmoothTail; general twists in the paper's class M are not covered by this module.

noncomputable def NairTenenbaum.rootSmoothTailBound {k r : ℕ} (A B κ : ℝ) (γ : Fin k → Fin r → ℕ) (C : Fin r → ℕ) (G : ℕ) : ℝ

Uniform constant in the root-weighted smooth-tail bound.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.rootSmoothTailBound_pos {k r : ℕ} {A B κ : ℝ} (hB : 0 ≤ B) (γ : Fin k → Fin r → ℕ) (C : Fin r → ℕ) (G : ℕ) : 0 < rootSmoothTailBound A B κ γ C G

theorem NairTenenbaum.truncated_rootTupleWeight_sum_le {k r : ℕ} {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (Q : Fin r → Polynomial ℤ) (D : ℕ) (N : ℕ+) (z : ℝ) : ∑ n ∈ weightUpTo γ D N with ↑(weightedMass γ n) ≤ z, rootTupleWeight γ F Q n ≤ ∑ m ∈ positiveUpTo z, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m

Removing the auxiliary finite mass bound only enlarges the truncated sum.

theorem NairTenenbaum.root_weight_smooth_tail_finite {k r : ℕ} {A B ε κ z x : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hx : 0 < x) (γ : 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) (D : ℕ) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m ≤ rootSmoothTailBound A B κ γ C G * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m

The complete finite root-vector tail estimate, with a sum truncated at z on the right and a constant independent of N, x, and z.

theorem NairTenenbaum.pnat_summable_and_tsum_le {f : ℕ+ → ℝ} {c : ℝ} (hf : ∀ (n : ℕ+), 0 ≤ f n) (hbound : ∀ (N : ℕ+), ∑ n ∈ Finset.Icc 1 N, f n ≤ c) : Summable f ∧ ∑' (n : ℕ+), f n ≤ c

Uniform bounds on initial positive-integer sums imply convergence and bound the infinite sum. This avoids using an unproved formal limit of partial sums.

theorem NairTenenbaum.root_weight_smooth_tail {k r : ℕ} {A B ε κ z x : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hx : 0 < x) (γ : 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) (D : ℕ) : have f := fun (m : ℕ+) => if ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m then weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m else 0; Summable f ∧ ∑' (m : ℕ+), f m ≤ rootSmoothTailBound A B κ γ C G * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m

Root-vector specialization of Lemma 2, as a convergent infinite series. The finite upper mass cutoff has disappeared, while the right-hand sum stops at z. The two coprimality restrictions are retained in weight.

theorem NairTenenbaum.PolynomialSystem.root_smooth_tail {k r : ℕ} (P : PolynomialSystem k r) {A B ε κ z x : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hx : 0 < x) (hzκ : 4 ^ (↑P.total.natDegree * κ) ≤ z) (hγε : ∀ (i : Fin r), ↑(totalExponent P.exponent i) * ε ≤ 1 / 8) : have f := fun (m : ℕ+) => if ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m then P.weight F m else 0; Summable f ∧ ∑' (m : ℕ+), f m ≤ rootSmoothTailBound A B κ P.exponent (fun (i : Fin r) => max (P.R i).natDegree (P.badDiscriminant ^ 3)) P.total.natDegree * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, P.weight F m

The infinite smooth tail for an actual polynomial system. Root-count bounds are discharged, and the constant is independent of the coefficients apart from the listed degree and restricted-discriminant data.