Products of one-variable admissible arithmetic functions

theorem NairTenenbaum.bigOmega_prod {ι : Type u_1} (s : Finset ι) (n : ι → ℕ) (hn : ∀ i ∈ s, n i ≠ 0) : bigOmega (∏ i ∈ s, n i) = ∑ i ∈ s, bigOmega (n i)

The total prime-factor count is additive over a finite nonzero product.

noncomputable def NairTenenbaum.productArithmeticMap {k : ℕ} (F : Fin k → ArithmeticMap 1) : ArithmeticMap k

The coordinate product of one-variable arithmetic functions.

Equations

• NairTenenbaum.productArithmeticMap F n = ∏ j : Fin k, F j fun (x : Fin 1) => n j

theorem NairTenenbaum.admissible_productArithmeticMap {k : ℕ} {A B σ : ℝ} {F : Fin k → ArithmeticMap 1} (hF : ∀ (j : Fin k), Admissible A B σ (F j)) : Admissible A (B ^ k) σ (productArithmeticMap F)

The product belongs to M_k(A,B^k,σ), with no change in the growth exponent.

theorem NairTenenbaum.extend_productArithmeticMap {k : ℕ} (F : Fin k → ArithmeticMap 1) (n : Fin k → ℕ) : extendArithmeticMap (productArithmeticMap F) n = ∏ j : Fin k, extendArithmeticMap (F j) fun (x : Fin 1) => n j

Zero extension commutes with the coordinate product, including tuples with vanishing polynomial values.