Exponent substitution and the dagger weight

The substitutions n', n'' and the lifted weight in §2, and the weight in equation (16). The exponent matrix and the discriminant are explicit arguments, allowing the combinatorial identities to be used independently of the polynomial factorization.

def NairTenenbaum.totalExponent {k r : ℕ} (γ : Fin k → Fin r → ℕ) (h : Fin r) : ℕ

The exponent of the hth irreducible factor in the total product.

Equations

• NairTenenbaum.totalExponent γ h = ∑ j : Fin k, γ j h

def NairTenenbaum.substitute {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) : Tuple k

The tuple n' in §2.

Equations

• NairTenenbaum.substitute γ n j = ∏ h : Fin r, n h ^ γ j h

def NairTenenbaum.weightedMass {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) : ℕ

The integer n'' in §2.

Equations

• NairTenenbaum.weightedMass γ n = ∏ h : Fin r, ↑(n h) ^ NairTenenbaum.totalExponent γ h

def NairTenenbaum.pullback {k r : ℕ} (γ : Fin k → Fin r → ℕ) (H : ArithmeticMap k) : ArithmeticMap r

Equation (15).

Equations

• NairTenenbaum.pullback γ H n = H (NairTenenbaum.substitute γ n)

@[simp]

theorem NairTenenbaum.substitute_one {k r : ℕ} (γ : Fin k → Fin r → ℕ) : substitute γ 1 = 1

@[simp]

theorem NairTenenbaum.substitute_mul {k r : ℕ} (γ : Fin k → Fin r → ℕ) (a b : Tuple r) : substitute γ (a * b) = substitute γ a * substitute γ b

theorem NairTenenbaum.mass_substitute {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) : mass (substitute γ n) = weightedMass γ n

theorem NairTenenbaum.weightedMass_pos {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) : 0 < weightedMass γ n

@[simp]

theorem NairTenenbaum.weightedMass_one {k r : ℕ} (γ : Fin k → Fin r → ℕ) : weightedMass γ 1 = 1

@[simp]

theorem NairTenenbaum.weightedMass_mul {k r : ℕ} (γ : Fin k → Fin r → ℕ) (a b : Tuple r) : weightedMass γ (a * b) = weightedMass γ a * weightedMass γ b

theorem NairTenenbaum.substitute_coprime {k r : ℕ} (γ : Fin k → Fin r → ℕ) {a b : Tuple r} (h : ∀ (i j : Fin r), (↑(a i)).Coprime ↑(b j)) : Coprime (substitute γ a) (substitute γ b)

Distinct tuples need cross-coordinate coprimality before substitution.

def NairTenenbaum.identityExponents (k : ℕ) (j h : Fin k) : ℕ

Identity exponent matrix, the irreducible pairwise coprime case.

Equations

• NairTenenbaum.identityExponents k j h = if j = h then 1 else 0

@[simp]

theorem NairTenenbaum.substitute_identity {k : ℕ} (n : Tuple k) : substitute (identityExponents k) n = n

@[simp]

theorem NairTenenbaum.totalExponent_identity {k : ℕ} (h : Fin k) : totalExponent (identityExponents k) h = 1

@[simp]

theorem NairTenenbaum.weightedMass_identity {k : ℕ} (n : Tuple k) : weightedMass (identityExponents k) n = mass n

def NairTenenbaum.Dagger {r : ℕ} (D : ℕ) (n : Tuple r) : Prop

The dagger in (16): pairwise coprimality and coprimality with |D*|.

Equations

• NairTenenbaum.Dagger D n = ((∀ (i j : Fin r), i ≠ j → (↑(n i)).Coprime ↑(n j)) ∧ ∀ (i : Fin r), (↑(n i)).Coprime D)

def NairTenenbaum.tupleBox (r : ℕ) (N : ℕ+) : Finset (Tuple r)

All positive tuples with each coordinate at most N.

Equations

• NairTenenbaum.tupleBox r N = Fintype.piFinset fun (x : Fin r) => Finset.Icc 1 N

@[simp]

theorem NairTenenbaum.mem_tupleBox {r : ℕ} {N : ℕ+} {n : Tuple r} : n ∈ tupleBox r N ↔ ∀ (h : Fin r), n h ≤ N

noncomputable def NairTenenbaum.weightFiber {k r : ℕ} (γ : Fin k → Fin r → ℕ) (D : ℕ) (N : ℕ+) : Finset (Tuple r)

Tuples in the fiber of n'', subject to the dagger conditions.

Equations

• NairTenenbaum.weightFiber γ D N = {n ∈ NairTenenbaum.tupleBox r N | NairTenenbaum.weightedMass γ n = ↑N ∧ NairTenenbaum.Dagger D n}

noncomputable def NairTenenbaum.weight {k r : ℕ} (γ : Fin k → Fin r → ℕ) (D : ℕ) (F : ArithmeticMap k) (θ : Fin r → ℕ → ℝ) (N : ℕ+) : ℝ

Equation (16), for a positive integer argument.

Equations

• NairTenenbaum.weight γ D F θ N = ∑ n ∈ NairTenenbaum.weightFiber γ D N, NairTenenbaum.pullback γ F n * ∏ h : Fin r, θ h ↑(n h) / ↑↑(n h)

theorem NairTenenbaum.coordinate_le_weightedMass {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (h : Fin r), 0 < totalExponent γ h) (n : Tuple r) (i : Fin r) : ↑(n i) ≤ weightedMass γ n

theorem NairTenenbaum.mem_weightFiber {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (h : Fin r), 0 < totalExponent γ h) (D : ℕ) (N : ℕ+) (n : Tuple r) : n ∈ weightFiber γ D N ↔ weightedMass γ n = ↑N ∧ Dagger D n

No tuples are lost by the finite box in the definition of the weight.

theorem NairTenenbaum.weight_nonneg {k r : ℕ} (γ : Fin k → Fin r → ℕ) (D : ℕ) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) {θ : Fin r → ℕ → ℝ} (hθ : ∀ (h : Fin r) (n : ℕ), 0 ≤ θ h n) (N : ℕ+) : 0 ≤ weight γ D F θ N

theorem NairTenenbaum.weightFiber_one_variable (D : ℕ) (N : ℕ+) : weightFiber (identityExponents 1) D N = if (↑N).Coprime D then {fun (x : Fin 1) => N} else ∅

In one variable the fiber has exactly one element when it is coprime to D.

theorem NairTenenbaum.weight_one_variable (D : ℕ) (F : ArithmeticMap 1) (θ : Fin 1 → ℕ → ℝ) (N : ℕ+) : weight (identityExponents 1) D F θ N = if (↑N).Coprime D then (F fun (x : Fin 1) => N) * θ 0 ↑N / ↑↑N else 0

The exact one-variable specialization of (16), including the dagger restriction.