Summing densities of disjoint congruence conditions

The exact CRT interval count, with its fixed remainder, implies density comparison for any finite disjoint collection of congruence conditions. This avoids choosing a common modulus or lifting residue representatives.

theorem NairTenenbaum.le_of_nat_mul_le_add {u v C : ℝ} (H : ∀ (N : ℕ), ↑N * u ≤ ↑N * v + C) : u ≤ v

A bounded additive remainder disappears when a counting inequality holds for every natural interval length.

noncomputable def NairTenenbaum.jointRootDensity {ι : Type u_1} [Fintype ι] (Q : ι → Polynomial ℤ) (q : ι → ℕ) : ℝ

Root density for simultaneous polynomial congruences at coprime moduli.

Equations

• NairTenenbaum.jointRootDensity Q q = ∏ i : ι, ↑(NairTenenbaum.rootCount (Q i) (q i)) / ↑(q i)

theorem NairTenenbaum.jointCongruenceCount_density_error {ι : Type u_1} [Fintype ι] (Q : ι → Polynomial ℤ) (q : ι → ℕ) (hq : ∀ (i : ι), 0 < q i) (hcop : Pairwise fun (i j : ι) => (q i).Coprime (q j)) (N : ℕ) : |↑(jointCongruenceCount Q q 0 ↑N) - ↑N * jointRootDensity Q q| ≤ ∏ i : ι, ↑(rootCount (Q i) (q i))

theorem NairTenenbaum.sum_jointRootDensity_le {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (S : Finset α) (Q : α → ι → Polynomial ℤ) (q : α → ι → ℕ) (hq : ∀ s ∈ S, ∀ (i : ι), 0 < q s i) (hcop : ∀ s ∈ S, Pairwise fun (i j : ι) => (q s i).Coprime (q s j)) (R : κ → Polynomial ℤ) (m : κ → ℕ) (hm : ∀ (i : κ), 0 < m i) (hmCop : Pairwise fun (i j : κ) => (m i).Coprime (m j)) (hdisjoint : ∀ s ∈ S, ∀ s' ∈ S, s ≠ s' → ∀ (t : ℤ), (∀ (i : ι), ↑(q s i) ∣ Polynomial.eval t (Q s i)) → ¬∀ (i : ι), ↑(q s' i) ∣ Polynomial.eval t (Q s' i)) (hsub : ∀ s ∈ S, ∀ (t : ℤ), (∀ (i : ι), ↑(q s i) ∣ Polynomial.eval t (Q s i)) → ∀ (i : κ), ↑(m i) ∣ Polynomial.eval t (R i)) : ∑ s ∈ S, jointRootDensity (Q s) (q s) ≤ jointRootDensity R m

A disjoint family of joint congruence conditions has total density at most any joint condition containing their union.