Truncated dagger tuples and the weight sum

The finite domains used in the global comparison, their closure under whole prime-power removal, and the exact reindexing of equation (16).

theorem NairTenenbaum.unitaryPart_dvd (n : ℕ+) (s : Finset ℕ) : ↑(unitaryPart n s) ∣ ↑n

theorem NairTenenbaum.unitaryRest_dvd (n : ℕ+) (s : Finset ℕ) : ↑(unitaryRest n s) ∣ ↑n

theorem NairTenenbaum.Dagger.of_coordinate_dvd {r D : ℕ} {n m : Tuple r} (hn : Dagger D n) (hm : ∀ (i : Fin r), ↑(m i) ∣ ↑(n i)) : Dagger D m

theorem NairTenenbaum.Dagger.of_tupleUnitaryRest {r D : ℕ} {n : Tuple r} (hn : Dagger D n) (t : Fin r → Finset ℕ) : Dagger D (tupleUnitaryRest n t)

theorem NairTenenbaum.Dagger.of_tupleUnitaryPart {r D : ℕ} {n : Tuple r} (hn : Dagger D n) (t : Fin r → Finset ℕ) : Dagger D (tupleUnitaryPart n t)

theorem NairTenenbaum.Dagger.unitary_cross_coprime {r D : ℕ} {n : Tuple r} (hn : Dagger D n) (t : Fin r → Finset ℕ) (i j : Fin r) : (↑(tupleUnitaryPart n t i)).Coprime ↑(tupleUnitaryRest n t j)

Independently chosen coordinate splittings are cross-coprime on dagger tuples.

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

Dagger tuples with weighted mass at most the specified cutoff.

Equations

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

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

theorem NairTenenbaum.weightUpTo_coordinate_le {k r : ℕ} (γ : Fin k → Fin r → ℕ) (D : ℕ) (N : ℕ+) {n : Tuple r} (hn : n ∈ weightUpTo γ D N) (i : Fin r) : n i ≤ N

theorem NairTenenbaum.weightedMass_unitaryRest_le {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) (t : Fin r → Finset ℕ) : weightedMass γ (tupleUnitaryRest n t) ≤ weightedMass γ n

theorem NairTenenbaum.tupleUnitaryRest_mem_weightUpTo {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (N : ℕ+) {n : Tuple r} (hn : n ∈ weightUpTo γ D N) (t : Fin r → Finset ℕ) : tupleUnitaryRest n t ∈ weightUpTo γ D N

theorem NairTenenbaum.sum_weight_eq_sum_weightUpTo {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (F : ArithmeticMap k) (θ : Fin r → ℕ → ℝ) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N, weight γ D F θ m = ∑ n ∈ weightUpTo γ D N, pullback γ F n * ∏ i : Fin r, θ i ↑(n i) / ↑↑(n i)

Every original fiber sum is retained exactly once by the truncated tuple sum.