Corollary 3: products of arithmetic functions on coprime polynomials

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

The left side of Corollary 3, with zero extension at polynomial roots.

Equations

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

theorem NairTenenbaum.shortSum_productArithmeticMap {k : ℕ} (Q : Fin k → Polynomial ℤ) (F : Fin k → ArithmeticMap 1) (x y : ℝ) : shortSum Q (productArithmeticMap F) x y = productShortSum Q F x y

def NairTenenbaum.CorollaryThree : Prop

Corollary 3, with constants chosen before the polynomial family and the arithmetic functions. The irreducible factorization data are supplied through PolynomialSystem, as in the current Theorem 1 interface.

Equations

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

theorem NairTenenbaum.corollaryThree : CorollaryThree

Proof of Corollary 3. The density comparison is applied to entire substitution fibers, so every original argument is counted only once.