Simultaneous polynomial congruences #
The Chinese remainder theorem gives the exact density for different polynomial conditions at pairwise coprime moduli. The bad-prime modulus may be a least common multiple; its coordinates need not be mutually coprime.
noncomputable def
NairTenenbaum.jointResidueSet
{ι : Type u_1}
[Fintype ι]
(Q : ι → Polynomial ℤ)
(q : ι → ℕ)
[∀ (i : ι), NeZero (q i)]
(hcop : Pairwise fun (i j : ι) => (q i).Coprime (q j))
:
The joint residue set, obtained from the product of the individual root sets.
Equations
- NairTenenbaum.jointResidueSet Q q hcop = Finset.image (⇑(ZMod.prodEquivPi q hcop).symm) (Fintype.piFinset fun (i : ι) => NairTenenbaum.residueRootSet (Q i) (q i))
Instances For
theorem
NairTenenbaum.jointResidueSet_card
{ι : Type u_1}
[Fintype ι]
(Q : ι → Polynomial ℤ)
(q : ι → ℕ)
[∀ (i : ι), NeZero (q i)]
(hcop : Pairwise fun (i j : ι) => (q i).Coprime (q j))
:
theorem
NairTenenbaum.cast_mem_jointResidueSet
{ι : Type u_1}
[Fintype ι]
(Q : ι → Polynomial ℤ)
(q : ι → ℕ)
[∀ (i : ι), NeZero (q i)]
(hcop : Pairwise fun (i j : ι) => (q i).Coprime (q j))
(n : ℤ)
:
noncomputable def
NairTenenbaum.jointCongruenceCount
{ι : Type u_1}
[Fintype ι]
(Q : ι → Polynomial ℤ)
(q : ι → ℕ)
(a b : ℤ)
:
The number of integers in an interval satisfying all polynomial congruences.
Equations
- NairTenenbaum.jointCongruenceCount Q q a b = {n ∈ Finset.Ioc a b | ∀ (i : ι), ↑(q i) ∣ Polynomial.eval n (Q i)}.card
Instances For
theorem
NairTenenbaum.jointCongruenceCount_le
{ι : Type u_1}
[Fintype ι]
(Q : ι → Polynomial ℤ)
(q : ι → ℕ)
(hq : ∀ (i : ι), 0 < q i)
(hcop : Pairwise fun (i j : ι) => (q i).Coprime (q j))
(a b : ℤ)
(hab : a ≤ b)
(hsize : ∏ i : ι, ↑(q i) ≤ ↑b - ↑a)
:
The residue-class error is absorbed whenever the modulus fits in the interval.
noncomputable def
NairTenenbaum.mixedCongruenceCount
{r : ℕ}
(Q : Polynomial ℤ)
(R : Fin r → Polynomial ℤ)
(d : ℕ)
(m : Tuple r)
(a b : ℤ)
:
A bad-prime modulus and the remaining coprime polynomial conditions.
Equations
- NairTenenbaum.mixedCongruenceCount Q R d m a b = NairTenenbaum.jointCongruenceCount (Fin.cons Q R) (Fin.cons d fun (i : Fin r) => ↑(m i)) a b
Instances For
theorem
NairTenenbaum.mixedCongruenceCount_le
{r : ℕ}
(Q : Polynomial ℤ)
(R : Fin r → Polynomial ℤ)
{d : ℕ}
(hd : 0 < d)
(m : Tuple r)
(hpair : Pairwise fun (i j : Fin r) => (↑(m i)).Coprime ↑(m j))
(hcross : ∀ (i : Fin r), d.Coprime ↑(m i))
(a b : ℤ)
(hab : a ≤ b)
(hsize : ↑d * ↑(mass m) ≤ ↑b - ↑a)
:
theorem
NairTenenbaum.PolynomialSystem.tupleLCM_dvd_radical_eval
{k r : ℕ}
(P : PolynomialSystem k r)
(m : Tuple r)
(a : ℤ)
(hm : ∀ (i : Fin r), ↑↑(m i) ∣ Polynomial.eval a (P.R i))
:
Simultaneous factor divisibility implies radical divisibility at the LCM.
theorem
NairTenenbaum.PolynomialSystem.jointCongruenceCount_le_mixed
{k r : ℕ}
(P : PolynomialSystem k r)
(u v : Tuple r)
(a b : ℤ)
:
jointCongruenceCount P.R (fun (i : Fin r) => ↑((u * v) i)) a b ≤ mixedCongruenceCount P.radical P.R (tupleLCM u) v a b
The full bad-prime part is kept as an LCM congruence while each good coordinate keeps its own irreducible-factor congruence.