Least common multiples and bad-prime mass

Coordinates supported at bad primes need not be coprime. Their simultaneous congruence conditions have least common multiple as modulus. The product of fractional auxiliary series bounds the associated mass uniformly.

def NairTenenbaum.tupleLCM {r : ℕ} (n : Tuple r) : ℕ

The least common multiple of the coordinates of a positive integer tuple.

Equations

• NairTenenbaum.tupleLCM n = Finset.univ.lcm fun (i : Fin r) => ↑(n i)

theorem NairTenenbaum.tupleLCM_pos {r : ℕ} (n : Tuple r) : 0 < tupleLCM n

theorem NairTenenbaum.coordinate_dvd_tupleLCM {r : ℕ} (n : Tuple r) (i : Fin r) : ↑(n i) ∣ tupleLCM n

theorem NairTenenbaum.tupleLCM_dvd_mass {r : ℕ} (n : Tuple r) : tupleLCM n ∣ mass n

theorem NairTenenbaum.mass_le_tupleLCM_pow {r G : ℕ} (n : Tuple r) (hr : r ≤ G) : mass n ≤ tupleLCM n ^ G

theorem NairTenenbaum.mass_rpow_le_tupleLCM {r G : ℕ} (n : Tuple r) (hG : 0 < G) (hr : r ≤ G) : ↑(mass n) ^ (1 / ↑G) ≤ ↑(tupleLCM n)

theorem NairTenenbaum.tupleLCM_mem_factoredNumbers {r : ℕ} (n : Tuple r) (s : Finset ℕ) (hn : ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers s) : tupleLCM n ∈ Nat.factoredNumbers s

theorem NairTenenbaum.auxiliary_prod_div_tupleLCM_le {r G : ℕ} {A B ε : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (η : Fin r → ℕ) (n : Tuple r) (hG : 0 < G) (hr : r ≤ G) : (∏ i : Fin r, auxiliary A B ε (η i) ↑(n i)) / ↑(tupleLCM n) ≤ ∏ i : Fin r, fractionalAuxiliary A B ε (1 / ↑G) (η i) ↑(n i)

The least-common-multiple density is bounded by a product of fractional coordinate densities. No pairwise coprimality is assumed.

theorem NairTenenbaum.rootCount_factored_le (Q : Polynomial ℤ) (s : Finset ℕ) (C : ℕ) (hC : 1 ≤ C) (hρ : ∀ p ∈ s, Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) {n : ℕ} (hn : n ∈ Nat.factoredNumbers s) : rootCount Q n ≤ C ^ (Finset.filter Nat.Prime s).card

A uniform local prime-power root bound gives a bound on every integer supported by the same finite set of primes.

theorem NairTenenbaum.PolynomialSystem.radical_rootCount_bad_supported {k r : ℕ} (P : PolynomialSystem k r) {n : ℕ} (hn : n ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) : rootCount P.radical n ≤ (P.badDiscriminant ^ 3) ^ P.badDiscriminant.primeFactors.card

The radical's root count on a bad-prime-supported modulus is bounded solely by the restricted discriminant.

theorem NairTenenbaum.sum_prod_fractionalAuxiliary_le {r G : ℕ} {A B ε σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (hr : r ≤ G) (η : Fin r → ℕ) (θ : Fin r → ℝ) (hη : ∀ (i : Fin r), ↑(η i) * ε - θ i ≤ σ) (s : Finset ℕ) (S : Finset (Tuple r)) (N : ℕ+) (hbox : ∀ n ∈ S, ∀ (i : Fin r), n i ≤ N) (hs : ∀ n ∈ S, ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers s) : ∑ n ∈ S, ∏ i : Fin r, fractionalAuxiliary A B ε (θ i) (η i) ↑(n i) ≤ (B / (1 - 2 ^ σ)) ^ (G * (Finset.filter Nat.Prime s).card)

Sum a product of fractional auxiliary weights over any supported finite set of tuples, using a common geometric exponent gap.

theorem NairTenenbaum.auxiliary_tupleLCM_sum_le {r G : ℕ} {A B ε σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (hG : 0 < G) (hr : r ≤ G) (η : Fin r → ℕ) (hη : ∀ (i : Fin r), ↑(η i) * ε - 1 / ↑G ≤ σ) (s : Finset ℕ) (S : Finset (Tuple r)) (N : ℕ+) (hbox : ∀ n ∈ S, ∀ (i : Fin r), n i ≤ N) (hs : ∀ n ∈ S, ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers s) : ∑ n ∈ S, (∏ i : Fin r, auxiliary A B ε (η i) ↑(n i)) / ↑(tupleLCM n) ≤ (B / (1 - 2 ^ σ)) ^ (G * (Finset.filter Nat.Prime s).card)

A finite sum over arbitrary bad-prime tuples is bounded independently of its coordinate cutoff.

noncomputable def NairTenenbaum.badPrimeTupleKernel {r : ℕ} (A B ε : ℝ) (η : Fin r → ℕ) (Q : Polynomial ℤ) (n : Tuple r) : ℝ

The cost of a bad-prime tuple, retaining a congruence density for its least common multiple instead of discarding the removed congruences.

Equations

• NairTenenbaum.badPrimeTupleKernel A B ε η Q n = (∏ i : Fin r, NairTenenbaum.auxiliary A B ε (η i) ↑(n i)) * ↑(NairTenenbaum.rootCount Q (NairTenenbaum.tupleLCM n)) / ↑(NairTenenbaum.tupleLCM n)

theorem NairTenenbaum.badPrimeTupleKernel_nonneg {r : ℕ} {A B ε : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (η : Fin r → ℕ) (Q : Polynomial ℤ) (n : Tuple r) : 0 ≤ badPrimeTupleKernel A B ε η Q n

noncomputable def NairTenenbaum.badPrimeMassBound (B : ℝ) (g D : ℕ) : ℝ

Uniform bound for the total mass of the bad-prime kernel.

Equations

• NairTenenbaum.badPrimeMassBound B g D = ↑((D ^ 3) ^ D.primeFactors.card) * (B / (1 - 2 ^ (-7 / (8 * ↑g)))) ^ (g * D.primeFactors.card)

theorem NairTenenbaum.badPrimeMassBound_pos {B : ℝ} (hB : 0 < B) {g D : ℕ} (hg : 0 < g) (hD : 0 < D) : 0 < badPrimeMassBound B g D

theorem NairTenenbaum.badPrime_exponent_gap {g η : ℕ} (hg : 0 < g) (hη : η ≤ g) {ε : ℝ} (hε : 0 ≤ ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) : ↑η * ε - 1 / ↑g ≤ -7 / (8 * ↑g)

The growth condition of Theorem 1 leaves a fixed geometric gap in the bad-prime series, even when all coordinates have large valuations together.

theorem NairTenenbaum.PolynomialSystem.badPrimeTupleKernel_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)) (N : ℕ+) (hbox : ∀ n ∈ S, ∀ (i : Fin r), n i ≤ N) (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

All bad-prime valuations can be summed at a cost depending only on the total degree, the growth constant B, and the restricted discriminant.