Polynomial families in §2

Factorizations retain unit signs, since the left side of Theorem 1 uses absolute values. The factors are irreducible over ℚ and pairwise nonassociated there.

structure NairTenenbaum.PolynomialSystem (k r : ℕ) : Type

The data of equation (9), including its arithmetic hypotheses.

• Q : Fin k → Polynomial ℤ

  The original integer polynomial family.

• R : Fin r → Polynomial ℤ

  The distinct rationally irreducible factors.

• exponent : Fin k → Fin r → ℕ

  Multiplicity of each irreducible factor in each original polynomial.

• sign : Fin k → ℤ

  The unit coefficient in each polynomial's factorization.

• sign_abs (j : Fin k) : (self.sign j).natAbs = 1
• factorization (j : Fin k) : self.Q j = Polynomial.C (self.sign j) * ∏ h : Fin r, self.R h ^ self.exponent j h
• irreducible (h : Fin r) : Irreducible (Polynomial.map (Int.castRingHom ℚ) (self.R h))
• nonassociated (i j : Fin r) : i ≠ j → ¬Associated (Polynomial.map (Int.castRingHom ℚ) (self.R i)) (Polynomial.map (Int.castRingHom ℚ) (self.R j))
• exponent_pos (h : Fin r) : 0 < totalExponent self.exponent h
• noFixedPrime : NoFixedPrimeDivisor (∏ j : Fin k, self.Q j)

noncomputable def NairTenenbaum.PolynomialSystem.total {k r : ℕ} (P : PolynomialSystem k r) : Polynomial ℤ

The product of the original polynomials of the system.

Equations

• P.total = ∏ j : Fin k, P.Q j

noncomputable def NairTenenbaum.PolynomialSystem.radical {k r : ℕ} (P : PolynomialSystem k r) : Polynomial ℤ

The product of the distinct irreducible factors of the system.

Equations

• P.radical = ∏ h : Fin r, P.R h

noncomputable def NairTenenbaum.PolynomialSystem.discriminant {k r : ℕ} (P : PolynomialSystem k r) : ℕ

Absolute discriminant |D*|.

Equations

• P.discriminant = P.radical.discr.natAbs

noncomputable def NairTenenbaum.PolynomialSystem.badDiscriminant {k r : ℕ} (P : PolynomialSystem k r) : ℕ

The factor D in §2, retaining exactly the bad primes where Q has roots.

Equations

• P.badDiscriminant = ∏ p ∈ P.discriminant.primeFactors with NairTenenbaum.rootCount P.total p ≠ 0, p ^ P.discriminant.factorization p

noncomputable def NairTenenbaum.PolynomialSystem.rootVector {k r : ℕ} (P : PolynomialSystem k r) (h : Fin r) (n : ℕ) : ℝ

The root count vector in (10).

Equations

• P.rootVector h n = ↑(NairTenenbaum.rootCount (P.R h) n)

noncomputable def NairTenenbaum.PolynomialSystem.weight {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (N : ℕ+) : ℝ

The weight (16) for the actual factorization of Q.

Equations

• P.weight F N = NairTenenbaum.weight P.exponent P.discriminant F P.rootVector N

theorem NairTenenbaum.PolynomialSystem.weight_nonneg {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (N : ℕ+) : 0 ≤ P.weight F N

theorem NairTenenbaum.PolynomialSystem.abs_eval_factorization {k r : ℕ} (P : PolynomialSystem k r) (j : Fin k) (n : ℤ) : (Polynomial.eval n (P.Q j)).natAbs = ∏ h : Fin r, (Polynomial.eval n (P.R h)).natAbs ^ P.exponent j h

theorem NairTenenbaum.PolynomialSystem.badDiscriminant_pos {k r : ℕ} (P : PolynomialSystem k r) : 0 < P.badDiscriminant

def NairTenenbaum.polynomialHeight (Q : Polynomial ℤ) : ℕ

Coefficient height ‖Q‖ = max_i |a_i|.

Equations

• NairTenenbaum.polynomialHeight Q = Q.support.sup fun (i : ℕ) => (Q.coeff i).natAbs

noncomputable def NairTenenbaum.extendArithmeticMap {k : ℕ} (F : ArithmeticMap k) (n : Fin k → ℕ) : ℝ

Extension by zero when a coordinate is zero. This makes polynomial-root terms explicit; on positive tuples it is precisely the original arithmetic function.

Equations

• NairTenenbaum.extendArithmeticMap F n = if h : ∀ (j : Fin k), 0 < n j then F fun (j : Fin k) => ⟨n j, ⋯⟩ else 0

@[simp]

theorem NairTenenbaum.extendArithmeticMap_coe {k : ℕ} (F : ArithmeticMap k) (n : Tuple k) : (extendArithmeticMap F fun (j : Fin k) => ↑(n j)) = F n

theorem NairTenenbaum.extendArithmeticMap_nonneg {k : ℕ} {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (n : Fin k → ℕ) : 0 ≤ extendArithmeticMap F n

noncomputable def NairTenenbaum.shortInterval (x y : ℝ) : Finset ℕ

Natural numbers in (x,x+y], for the positive real ranges in the theorems.

Equations

• NairTenenbaum.shortInterval x y = Finset.Ioc ⌊x⌋₊ ⌊x + y⌋₊

noncomputable def NairTenenbaum.shortSum {k : ℕ} (Q : Fin k → Polynomial ℤ) (F : ArithmeticMap k) (x y : ℝ) : ℝ

Left side of (18).

Equations

• NairTenenbaum.shortSum Q F x y = ∑ n ∈ NairTenenbaum.shortInterval x y, NairTenenbaum.extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval (↑n) (Q j)).natAbs

noncomputable def NairTenenbaum.positiveUpTo (x : ℝ) : Finset ℕ+

Positive integers at most x. The filter also handles x < 1 correctly.

Equations

• NairTenenbaum.positiveUpTo x = {n ∈ Finset.Icc 1 ⌊x⌋₊.toPNat' | ↑↑n ≤ x}

@[simp]

theorem NairTenenbaum.mem_positiveUpTo (n : ℕ+) (x : ℝ) : n ∈ positiveUpTo x ↔ ↑↑n ≤ x

theorem NairTenenbaum.positiveUpTo_eq_Icc {x : ℝ} (hx : 1 ≤ x) : positiveUpTo x = Finset.Icc 1 ⌊x⌋₊.toPNat'

theorem NairTenenbaum.positiveUpTo_eq_empty {x : ℝ} (hx : x < 1) : positiveUpTo x = ∅

noncomputable def NairTenenbaum.mainTerm {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (x y : ℝ) : ℝ

The right side of (18), without the implicit constant.

Equations

• NairTenenbaum.mainTerm P F x y = y * NairTenenbaum.sieveProduct P.total x * ∑ n ∈ NairTenenbaum.positiveUpTo x, P.weight F n

theorem NairTenenbaum.mainTerm_nonneg {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (x : ℝ) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ mainTerm P F x y