Corrected comparison for a single arithmetic variable

The finite convolution comparison and the weighted Euler-product bounds are instantiated with the paper's admissible functions, polynomial root counts, dagger restriction, and reciprocal-totient correction.

theorem NairTenenbaum.totientTwist_eq_radicalProduct (g : ℕ) {n : ℕ} (hn : n ≠ 0) : totientTwist g n = radicalProduct (fun (p : ℕ) => 1 + |totientTwist g p - 1|) n

The totient correction is a product of nonnegative prime increments.

theorem NairTenenbaum.Admissible.scalar_mul_le_auxiliary {A B ε : ℝ} {F : ArithmeticMap 1} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (a b : ℕ+) (hab : (↑a).Coprime ↑b) : (F fun (x : Fin 1) => a * b) ≤ auxiliary A B ε 1 ↑a * F fun (x : Fin 1) => b

Coprime multiplication is controlled by the actual auxiliary function.

theorem NairTenenbaum.Admissible.scalar_weight_mul_le {A B ε : ℝ} {F : ArithmeticMap 1} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (D : ℕ) (Q : Polynomial ℤ) (a b : ℕ+) (hab : (↑a).Coprime ↑b) : weight (identityExponents 1) D F (fun (x : Fin 1) (n : ℕ) => ↑(rootCount Q n)) (a * b) ≤ rootAuxiliary A B ε 1 Q ↑a * weight (identityExponents 1) D F (fun (x : Fin 1) (n : ℕ) => ↑(rootCount Q n)) b

The dagger-restricted scalar weight inherits a coprime majorant.

theorem NairTenenbaum.scalar_weight_twist (D : ℕ) (F : ArithmeticMap 1) (Q : Polynomial ℤ) (θ : ℕ → ℝ) (n : ℕ+) : weight (identityExponents 1) D F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount Q m) * θ m) n = weight (identityExponents 1) D F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount Q m)) n * θ ↑n

Multiplying the root vector by a scalar twist multiplies the scalar weight.

theorem NairTenenbaum.totient_kernelLocalError (A B ε : ℝ) (γ : ℕ) (Q : Polynomial ℤ) (g : ℕ) {p : ℕ} (hp : Nat.Prime p) : kernelLocalError (rootAuxiliary A B ε γ Q) (fun (p : ℕ) => |totientTwist g p - 1|) p = localComparisonError A B ε γ Q (totientTwist g) p

The generic convolution local error is precisely the repaired local error for the totient correction.

theorem NairTenenbaum.scalar_totient_comparison {A B ε : ℝ} {F : ArithmeticMap 1} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hε₁ : ε < 1) (D : ℕ) (Q : Polynomial ℤ) (g C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, weight (identityExponents 1) D F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount Q m) * totientTwist g m) n ≤ Real.exp (∑' (p : Nat.Primes), localComparisonError A B ε 1 Q (totientTwist g) ↑p) * ∑ n ∈ Finset.Icc 1 N, weight (identityExponents 1) D F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount Q m)) n

A proved replacement for the printed comparison in the scalar case. The coefficient is independent of N and of the admissible function F.

noncomputable def NairTenenbaum.scalarComparisonBound (B ε : ℝ) (g C : ℕ) : ℝ

A comparison constant expressed solely in the growth parameters, the power of the totient correction, and a uniform root-count bound.

Equations

• NairTenenbaum.scalarComparisonBound B ε g C = Real.exp (2 * (2 ^ g - 1) * ↑C * B / (1 - 2 ^ (ε - 1)) * ∑' (n : ℕ), ↑n ^ (ε - 2))

theorem NairTenenbaum.scalarComparisonBound_pos (B ε : ℝ) (g C : ℕ) : 0 < scalarComparisonBound B ε g C

theorem NairTenenbaum.scalar_totient_comparison_uniform {A B ε : ℝ} {F : ArithmeticMap 1} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hε₁ : ε < 1) (D : ℕ) (Q : Polynomial ℤ) (g C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, weight (identityExponents 1) D F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount Q m) * totientTwist g m) n ≤ scalarComparisonBound B ε g C * ∑ n ∈ Finset.Icc 1 N, weight (identityExponents 1) D F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount Q m)) n

The scalar comparison with a coefficient-independent explicit constant.

theorem NairTenenbaum.PolynomialSystem.factor_scalar_totient_comparison {k r : ℕ} (P : PolynomialSystem k r) {A B ε : ℝ} {F : ArithmeticMap 1} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hε₁ : ε < 1) (g : ℕ) (h : Fin r) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, NairTenenbaum.weight (identityExponents 1) P.discriminant F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount (P.R h) m) * totientTwist g m) n ≤ scalarComparisonBound B ε g (max (P.R h).natDegree (P.badDiscriminant ^ 3)) * ∑ n ∈ Finset.Icc 1 N, NairTenenbaum.weight (identityExponents 1) P.discriminant F (fun (x : Fin 1) (m : ℕ) => ↑(rootCount (P.R h) m)) n

Each actual irreducible polynomial factor satisfies the scalar comparison; no root-count estimate is left as an extra hypothesis.