Degree and discriminant uniformity of the smooth-tail constants

There are finitely many possible exponent totals and root bounds at a fixed total degree and restricted discriminant. A finite envelope of the explicit constants removes dependence on the individual factorization data. This does not require monotonicity of the auxiliary cutoff chosen by absorption.

def NairTenenbaum.exponentRow {r : ℕ} (η : Fin r → ℕ) : Fin 1 → Fin r → ℕ

Represent a list of coordinate totals by a one-row exponent matrix.

Equations

• NairTenenbaum.exponentRow η x✝ = η

@[simp]

theorem NairTenenbaum.totalExponent_exponentRow {r : ℕ} (η : Fin r → ℕ) (i : Fin r) : totalExponent (exponentRow η) i = η i

theorem NairTenenbaum.rootSmoothTailBound_congr_totals {k₁ k₂ r : ℕ} (A B κ : ℝ) (γ₁ : Fin k₁ → Fin r → ℕ) (γ₂ : Fin k₂ → Fin r → ℕ) (hγ : ∀ (i : Fin r), totalExponent γ₁ i = totalExponent γ₂ i) (C : Fin r → ℕ) (G : ℕ) : rootSmoothTailBound A B κ γ₁ C G = rootSmoothTailBound A B κ γ₂ C G

theorem NairTenenbaum.totientSmoothTailBound_congr_totals {k₁ k₂ r : ℕ} (A B κ : ℝ) (γ₁ : Fin k₁ → Fin r → ℕ) (γ₂ : Fin k₂ → Fin r → ℕ) (hγ : ∀ (i : Fin r), totalExponent γ₁ i = totalExponent γ₂ i) (C : Fin r → ℕ) (G g : ℕ) : totientSmoothTailBound A B κ γ₁ C G g = totientSmoothTailBound A B κ γ₂ C G g

noncomputable def NairTenenbaum.smoothTailUniformBound (A B κ : ℝ) (g D : ℕ) : ℝ

A finite envelope depending only on degree and restricted discriminant. The deliberately non-sharp constant simultaneously covers the root vector and the totient-modified root vector with exponent equal to total degree.

Equations

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

theorem NairTenenbaum.smoothTailUniformBound_pos (A B κ : ℝ) (g D : ℕ) : 0 < smoothTailUniformBound A B κ g D

theorem NairTenenbaum.smoothTailBounds_le_uniform {k r : ℕ} (A B κ : ℝ) (g D : ℕ) (γ : Fin k → Fin r → ℕ) (C : Fin r → ℕ) (hr : r ≤ g) (hγ : ∀ (i : Fin r), totalExponent γ i ≤ g) (hC : ∀ (i : Fin r), C i ≤ max g (D ^ 3)) : rootSmoothTailBound A B κ γ C g ≤ smoothTailUniformBound A B κ g D ∧ totientSmoothTailBound A B κ γ C g g ≤ smoothTailUniformBound A B κ g D

Every allowed tuple of factorization data occurs in the finite envelope.

theorem NairTenenbaum.PolynomialSystem.root_smooth_tail_uniform {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) (hgε : ↑P.total.natDegree * ε ≤ 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 ≤ smoothTailUniformBound A B κ P.total.natDegree P.badDiscriminant * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, P.weight F m

Root-vector smooth tail with a constant depending only on total degree and restricted discriminant among the polynomial data.

theorem NairTenenbaum.PolynomialSystem.totient_smooth_tail_uniform {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) (hgε : ↑P.total.natDegree * ε ≤ 1 / 8) : have f := fun (m : ℕ+) => if ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m then NairTenenbaum.weight P.exponent P.discriminant F (fun (i : Fin r) (m : ℕ) => P.rootVector i m * totientTwist P.total.natDegree m) m else 0; Summable f ∧ ∑' (m : ℕ+), f m ≤ smoothTailUniformBound A B κ P.total.natDegree P.badDiscriminant * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, P.weight F m

The totient-modified smooth tail with the exact uniformity required in the main theorem. Its right-hand weight is the original root vector.

theorem NairTenenbaum.smooth_exponent_of_theoremOne {g : ℕ} (hg : 0 < g) {ε δ : ℝ} (hε : 0 < ε) (hεg : ε < 1 / (8 * ↑g ^ 2)) (hδ : δ ≤ 1) : ↑g * (ε * δ / 3) ≤ 1 / 8

Theorem 1's admissibility exponent satisfies the fixed small-exponent condition needed by the smooth-tail argument.

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

The totient smooth tail can be used directly with Theorem 1's parameters, without any additional local growth or root-count assumptions.