Uniform comparison with an independent totient exponent

Prime arguments add one totient power without changing the original polynomial degrees or the admissibility exponent. Keeping these parameters separate avoids imposing a stronger growth assumption on the arithmetic map.

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

The comparison constant for a separately specified totient exponent.

Equations

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

theorem NairTenenbaum.totientExponentComparisonBound_pos (B ε : ℝ) (g h D : ℕ) : 0 < totientExponentComparisonBound B ε g h D

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

The degree and twist exponent are independent. Uniformity uses only the degree bound, twist exponent, growth parameters, and bad discriminant.

theorem NairTenenbaum.PolynomialSystem.totient_tuple_sum_le_exponent {k r : ℕ} (P : PolynomialSystem k r) {g : ℕ} (hdeg : P.total.natDegree ≤ g) {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hgε : ↑g * ε < 1) (h : ℕ) (N : ℕ+) : ∑ v ∈ weightUpTo P.exponent P.discriminant N, rootTupleWeight P.exponent F P.R v * ∏ i : Fin r, totientTwist h ↑(v i) ≤ totientExponentComparisonBound B ε g h P.badDiscriminant * ∑ n ∈ Finset.Icc 1 N, P.weight F n