Products on disjoint blocks of arithmetic coordinates

noncomputable def NairTenenbaum.appendArithmeticMap {k r : ℕ} (F : ArithmeticMap k) (H : ArithmeticMap r) : ArithmeticMap (k + r)

The arithmetic map obtained by adjoining the extra coordinate.

Equations

• NairTenenbaum.appendArithmeticMap F H n = (F fun (j : Fin k) => n (Fin.castAdd r j)) * H fun (i : Fin r) => n (Fin.natAdd k i)

theorem NairTenenbaum.mass_append_blocks {k r : ℕ} (n : Tuple (k + r)) : mass n = (mass fun (j : Fin k) => n (Fin.castAdd r j)) * mass fun (i : Fin r) => n (Fin.natAdd k i)

theorem NairTenenbaum.admissible_appendArithmeticMap {k r : ℕ} {A B C ε : ℝ} {F : ArithmeticMap k} {H : ArithmeticMap r} (hF : Admissible A B ε F) (hH : Admissible A C ε H) (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) : Admissible A (B * C) ε (appendArithmeticMap F H)

Independent coordinate blocks multiply the polynomial growth constants, while keeping a common exponent and prime-factor constant.

def NairTenenbaum.ScalarClassM (θ : ℕ → ℝ) : Prop

The paper's scalar class M: one prime-factor constant works for every positive polynomial-growth exponent, with the latter's constant allowed to vary.

Equations

• NairTenenbaum.ScalarClassM θ = ∃ (A : ℝ), 1 ≤ A ∧ ∀ (ε : ℝ), 0 < ε → ∃ (B : ℝ), 1 ≤ B ∧ NairTenenbaum.Admissible A B ε fun (n : NairTenenbaum.Tuple 1) => θ ↑(n 0)

theorem NairTenenbaum.scalarClassM_common {r : ℕ} {θ : Fin r → ℕ → ℝ} (hθ : ∀ (i : Fin r), ScalarClassM (θ i)) {ε : ℝ} (hε : 0 < ε) : ∃ (A : ℝ) (B : ℝ), 1 ≤ A ∧ 1 ≤ B ∧ ∀ (i : Fin r), Admissible A B ε fun (n : Tuple 1) => θ i ↑(n 0)

A finite family in M has common admissibility constants at any fixed positive exponent.