Arithmetic functions in Nair–Tenenbaum

Equation (1) and the basic consequences used in §2 of Short sums of certain arithmetic functions, Acta Math. 180 (1998), 119–144. Tuples take values in ℕ+, so zero is never silently admitted into the domain.

@[reducible, inline]

abbrev NairTenenbaum.Tuple (k : ℕ) : Type

A tuple of positive integers with a fixed number of coordinates.

Equations

• NairTenenbaum.Tuple k = (Fin k → ℕ+)

@[reducible, inline]

abbrev NairTenenbaum.ArithmeticMap (k : ℕ) : Type

A real-valued arithmetic function on positive integer tuples.

Equations

• NairTenenbaum.ArithmeticMap k = (NairTenenbaum.Tuple k → ℝ)

def NairTenenbaum.bigOmega (n : ℕ) : ℕ

Total number of prime factors, with multiplicity.

Equations

• NairTenenbaum.bigOmega n = n.primeFactorsList.length

@[simp]

theorem NairTenenbaum.bigOmega_one : bigOmega 1 = 0

theorem NairTenenbaum.bigOmega_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : bigOmega (m * n) = bigOmega m + bigOmega n

def NairTenenbaum.mass {k : ℕ} (n : Tuple k) : ℕ

Product of the coordinates of a positive tuple.

Equations

• NairTenenbaum.mass n = ∏ j : Fin k, ↑(n j)

theorem NairTenenbaum.mass_pos {k : ℕ} (n : Tuple k) : 0 < mass n

@[simp]

theorem NairTenenbaum.mass_mul {k : ℕ} (m n : Tuple k) : mass (m * n) = mass m * mass n

def NairTenenbaum.Coprime {k : ℕ} (m n : Tuple k) : Prop

Coprimality is coordinatewise, as in (1), not between the two total products.

Equations

• NairTenenbaum.Coprime m n = ∀ (j : Fin k), (↑(m j)).Coprime ↑(n j)

theorem NairTenenbaum.Coprime.symm {k : ℕ} {m n : Tuple k} (h : Coprime m n) : Coprime n m

@[simp]

theorem NairTenenbaum.coprime_one_right {k : ℕ} (m : Tuple k) : Coprime m 1

@[simp]

theorem NairTenenbaum.coprime_one_left {k : ℕ} (m : Tuple k) : Coprime 1 m

theorem NairTenenbaum.coprime_mul_right {k : ℕ} (a b c : Tuple k) : Coprime a (b * c) ↔ Coprime a b ∧ Coprime a c

theorem NairTenenbaum.coprime_mul_left {k : ℕ} (a b c : Tuple k) : Coprime (a * b) c ↔ Coprime a c ∧ Coprime b c

noncomputable def NairTenenbaum.growthBound {k : ℕ} (A B ε : ℝ) (m : Tuple k) : ℝ

The majorant in equation (1).

Equations

• NairTenenbaum.growthBound A B ε m = min (A ^ NairTenenbaum.bigOmega (NairTenenbaum.mass m)) (B * ↑(NairTenenbaum.mass m) ^ ε)

structure NairTenenbaum.Admissible {k : ℕ} (A B ε : ℝ) (F : ArithmeticMap k) : Prop

Membership of 𝓜ₖ(A,B,ε). Parameter ranges are supplied by individual theorems.

• nonneg (n : Tuple k) : 0 ≤ F n
• growth (m n : Tuple k) : Coprime m n → F (m * n) ≤ growthBound A B ε m * F n

theorem NairTenenbaum.growthBound_nonneg {k : ℕ} {A B ε : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (m : Tuple k) : 0 ≤ growthBound A B ε m

theorem NairTenenbaum.growthBound_mono {k : ℕ} {A B ε A' B' ε' : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAA : A ≤ A') (hBB : B ≤ B') (hε : ε ≤ ε') (m : Tuple k) : growthBound A B ε m ≤ growthBound A' B' ε' m

theorem NairTenenbaum.Admissible.mono {k : ℕ} {A B ε A' B' ε' : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (hAA : A ≤ A') (hBB : B ≤ B') (hε : ε ≤ ε') : Admissible A' B' ε' F

theorem NairTenenbaum.Admissible.le_at_one {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (n : Tuple k) : F n ≤ growthBound A B ε n * F 1

theorem NairTenenbaum.Admissible.eq_zero_of_one {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (h : F 1 = 0) : F = 0

theorem NairTenenbaum.Admissible.add {k : ℕ} {A B ε : ℝ} {F H : ArithmeticMap k} (hF : Admissible A B ε F) (hH : Admissible A B ε H) : Admissible A B ε (F + H)

theorem NairTenenbaum.Admissible.smul {k : ℕ} {A B ε c : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hc : 0 ≤ c) : Admissible A B ε fun (n : Tuple k) => c * F n

theorem NairTenenbaum.Admissible.rpow {k : ℕ} {A B ε t : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (ht : 0 ≤ t) : Admissible (A ^ t) (B ^ t) (ε * t) fun (n : Tuple k) => F n ^ t

Taking a nonnegative power preserves the arithmetic class with the expected change in its three parameters.