Exact progression identity for the original weights

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

Coprimality of the weighted mass is equivalent to coprimality in every irreducible coordinate. Positive exponents are essential in the reverse direction.

theorem NairTenenbaum.PolynomialSystem.dagger_affine_iff {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (n : Tuple r) (hqn : ∀ (i : Fin r), q.Coprime ↑(n i)) : Dagger (P.affine q a hq hqa).discriminant n ↔ Dagger P.discriminant n

On tuples coprime to the progression modulus, the dagger restrictions for the original and transformed discriminants coincide.

theorem NairTenenbaum.PolynomialSystem.affine_weight_of_coprime {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (F : ArithmeticMap k) (N : ℕ+) (hN : q.Coprime ↑N) : (P.affine q a hq hqa).weight F N = P.weight F N

On every mass coprime to q, both the fiber restriction and every root factor in the weight are unchanged by affine substitution.

theorem NairTenenbaum.PolynomialSystem.affine_weight_eq_zero {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (F : ArithmeticMap k) (N : ℕ+) (hN : ¬q.Coprime ↑N) : (P.affine q a hq hqa).weight F N = 0

If the mass shares a prime with q, one root factor vanishes in every summand, regardless of the dagger restriction.

theorem NairTenenbaum.PolynomialSystem.affine_weight {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (F : ArithmeticMap k) (N : ℕ+) : (P.affine q a hq hqa).weight F N = if q.Coprime ↑N then P.weight F N else 0

The exact identity used after equation (38): the transformed weight equals the original weight with the extra coprimality condition (N,q)=1.

theorem NairTenenbaum.PolynomialSystem.sum_affine_weight {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (F : ArithmeticMap k) (x : ℝ) : ∑ N ∈ positiveUpTo x, (P.affine q a hq hqa).weight F N = ∑ N ∈ positiveUpTo x with q.Coprime ↑N, P.weight F N