Root-density aggregation over exponent-substitution fibers

theorem NairTenenbaum.PolynomialSystem.factor_dvd_polynomial {k r : ℕ} (P : PolynomialSystem k r) (j : Fin k) (i : Fin r) (hi : 0 < P.exponent j i) : P.R i ∣ P.Q j

A factor with a positive exponent divides the corresponding polynomial.

theorem NairTenenbaum.PolynomialSystem.exponent_disjoint {k r : ℕ} (P : PolynomialSystem k r) (hcop : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (P.Q i)) (Polynomial.map (Int.castRingHom ℚ) (P.Q j))) {i j : Fin k} (hij : i ≠ j) (h : Fin r) : P.exponent i h = 0 ∨ P.exponent j h = 0

Pairwise coprime original polynomials have disjoint exponent supports.

theorem NairTenenbaum.PolynomialSystem.substitute_pairwise_coprime {k r : ℕ} (P : PolynomialSystem k r) (hcop : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (P.Q i)) (Polynomial.map (Int.castRingHom ℚ) (P.Q j))) (n : Tuple r) (hn : Pairwise fun (i j : Fin r) => (↑(n i)).Coprime ↑(n j)) : Pairwise fun (i j : Fin k) => (↑(substitute P.exponent n i)).Coprime ↑(substitute P.exponent n j)

Dagger tuples remain pairwise coprime after substitution into pairwise coprime original polynomials.

theorem NairTenenbaum.PolynomialSystem.substitute_dvd_eval {k r : ℕ} (P : PolynomialSystem k r) (n : Tuple r) (t : ℤ) (hn : ∀ (i : Fin r), ↑↑(n i) ∣ Polynomial.eval t (P.R i)) (j : Fin k) : ↑↑(substitute P.exponent n j) ∣ Polynomial.eval t (P.Q j)

Factor-value divisibility gives all the original polynomial congruences at the substituted moduli.

theorem NairTenenbaum.PolynomialSystem.sum_substitutionFiber_rootDensity_le {k r : ℕ} (P : PolynomialSystem k r) (S : Finset (Tuple r)) (hS : ∀ n ∈ S, Dagger P.discriminant n) (m : Tuple k) (hm : Pairwise fun (i j : Fin k) => (↑(m i)).Coprime ↑(m j)) (hsubst : ∀ n ∈ S, substitute P.exponent n = m) : ∑ n ∈ S, ∏ i : Fin r, ↑(rootCount (P.R i) ↑(n i)) / ↑↑(n i) ≤ ∏ j : Fin k, ↑(rootCount (P.Q j) ↑(m j)) / ↑↑(m j)

Aggregate all dagger tuples with the same substituted arguments before comparing with the joint root density of the original polynomials.