Summing bad-prime congruence contributions #
The complete bad-prime valuations have a uniform total cost when their joint congruence density is retained. This is the counting input for the corrected full-prime-power discriminant split.
theorem
NairTenenbaum.factoredNumbers_coprime_of_coprime
{D n m : ℕ}
(hn : n ∈ Nat.factoredNumbers D.primeFactors)
(hm : D.Coprime m)
:
n.Coprime m
theorem
NairTenenbaum.PolynomialSystem.badPrimeTupleKernel_sum_le_of_support
{k r : ℕ}
(P : PolynomialSystem k r)
{A B ε : ℝ}
(hA : 0 ≤ A)
(hB : 1 ≤ B)
(hε : 0 < ε)
(hg : 0 < P.total.natDegree)
(hsmall : ↑P.total.natDegree ^ 2 * ε ≤ 1 / 8)
(S : Finset (Tuple r))
(hs : ∀ n ∈ S, ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors)
:
∑ n ∈ S, badPrimeTupleKernel A B ε (totalExponent P.exponent) P.radical n ≤ badPrimeMassBound B P.total.natDegree P.badDiscriminant
theorem
NairTenenbaum.PolynomialSystem.badPrime_congruence_sum_le
{k r : ℕ}
(P : PolynomialSystem k r)
{A B ε : ℝ}
(hA : 0 ≤ A)
(hB : 1 ≤ B)
(hε : 0 < ε)
(hg : 0 < P.total.natDegree)
(hsmall : ↑P.total.natDegree ^ 2 * ε ≤ 1 / 8)
(S : Finset (Tuple r))
(v : Tuple r)
(hv : Dagger P.badDiscriminant v)
(hs : ∀ u ∈ S, ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors)
(a b : ℤ)
(hab : a ≤ b)
(hsize : ∀ u ∈ S, ↑(tupleLCM u) * ↑(mass v) ≤ ↑b - ↑a)
:
A uniform sum over bad-prime valuations, with the good-coordinate density left intact. The size hypothesis is on the actual combined congruence modulus.
theorem
NairTenenbaum.PolynomialSystem.badPrime_weighted_congruence_sum_le
{k r : ℕ}
(P : PolynomialSystem k r)
{A B ε : ℝ}
{F : ArithmeticMap k}
(hF : Admissible A B ε F)
(hA : 0 ≤ A)
(hB : 1 ≤ B)
(hε : 0 < ε)
(hg : 0 < P.total.natDegree)
(hsmall : ↑P.total.natDegree ^ 2 * ε ≤ 1 / 8)
(S : Finset (Tuple r))
(v : Tuple r)
(hv : Dagger P.badDiscriminant v)
(hs : ∀ u ∈ S, ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors)
(a b : ℤ)
(hab : a ≤ b)
(hsize : ∀ u ∈ S, ↑(tupleLCM u) * ↑(mass v) ≤ ↑b - ↑a)
:
∑ u ∈ S, pullback P.exponent F (u * v) * ↑(jointCongruenceCount P.R (fun (i : Fin r) => ↑((u * v) i)) a b) ≤ 2 * (↑b - ↑a) * badPrimeMassBound B P.total.natDegree P.badDiscriminant * rootTupleWeight P.exponent F P.R v
The same estimate with the original admissible arithmetic function.