Uniformity of the corrected comparison

The comparison constant is bounded using only total degree, growth parameters, and the restricted bad discriminant, as required by the main theorem.

theorem NairTenenbaum.scalarComparisonBound_one_le {B ε : ℝ} (hB : 0 ≤ B) (hε : ε < 1) (g C : ℕ) : 1 ≤ scalarComparisonBound B ε g C

theorem NairTenenbaum.scalarComparisonBound_mono {B ε₁ ε₂ : ℝ} (hB : 0 ≤ B) (hε : ε₁ ≤ ε₂) (hε₂ : ε₂ < 1) (g : ℕ) {C₁ C₂ : ℕ} (hC : C₁ ≤ C₂) : scalarComparisonBound B ε₁ g C₁ ≤ scalarComparisonBound B ε₂ g C₂

Monotonicity permits all coordinate exponents and root bounds to be replaced by the same total-degree bound.

noncomputable def NairTenenbaum.totientComparisonBound (B ε : ℝ) (g D : ℕ) : ℝ

The constant depends on the polynomial system only through degree and restricted discriminant.

Equations

• NairTenenbaum.totientComparisonBound B ε g D = NairTenenbaum.scalarComparisonBound B (↑g * ε) g (max g (D ^ 3)) ^ g

theorem NairTenenbaum.totientComparisonBound_pos (B ε : ℝ) (g D : ℕ) : 0 < totientComparisonBound B ε g D

theorem NairTenenbaum.PolynomialSystem.totient_comparison_uniform {k r : ℕ} (P : PolynomialSystem k r) {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hgε : ↑P.total.natDegree * ε < 1) (x : ℝ) : ∑ n ∈ positiveUpTo x, NairTenenbaum.weight P.exponent P.discriminant F (fun (i : Fin r) (m : ℕ) => P.rootVector i m * totientTwist P.total.natDegree m) n ≤ totientComparisonBound B ε P.total.natDegree P.badDiscriminant * ∑ n ∈ positiveUpTo x, P.weight F n

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

The small-exponent condition needed by the comparison follows from the parameters of Theorem 1.

theorem NairTenenbaum.PolynomialSystem.totient_comparison_theoremOne_parameters {k r : ℕ} (P : PolynomialSystem k r) {A B ε δ : ℝ} {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) (x : ℝ) : ∑ n ∈ positiveUpTo x, NairTenenbaum.weight P.exponent P.discriminant F (fun (i : Fin r) (m : ℕ) => P.rootVector i m * totientTwist P.total.natDegree m) n ≤ totientComparisonBound B (ε * δ / 3) P.total.natDegree P.badDiscriminant * ∑ n ∈ positiveUpTo x, P.weight F n

The comparison is directly available with Theorem 1's admissibility exponent; the extra local convergence condition is fully discharged.