Exponential moments for the full bad-prime tuple kernel

The mass lost during whole-prime-power removal is retained in a small positive moment. This allows a tail estimate for the original prefix mass, without a bounded-valuation assumption at bad primes.

theorem NairTenenbaum.auxiliary_tupleLCM_moment_le {k r G : ℕ} {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ : Fin k → Fin r → ℕ) (n : Tuple r) (hG : 0 < G) (hr : r ≤ G) : (∏ i : Fin r, auxiliary A B ε (totalExponent γ i) ↑(n i)) / ↑(tupleLCM n) * ↑(weightedMass γ n) ^ β ≤ ∏ i : Fin r, fractionalAuxiliary A B ε (1 / ↑G - ↑(totalExponent γ i) * β) (totalExponent γ i) ↑(n i)

theorem NairTenenbaum.auxiliary_tupleLCM_moment_sum_le {k r G : ℕ} {A B ε β σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (hG : 0 < G) (hr : r ≤ G) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), ↑(totalExponent γ 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 ε (totalExponent γ i) ↑(n i)) / ↑(tupleLCM n) * ↑(weightedMass γ n) ^ β ≤ (B / (1 - 2 ^ σ)) ^ (G * (Finset.filter Nat.Prime s).card)

Uniform finite moment bound with an arbitrary fixed exponent gap.

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

Uniform bound for moments of the full bad-prime tuple kernel.

Equations

• NairTenenbaum.badPrimeMomentBound B g D = ↑((D ^ 3) ^ D.primeFactors.card) * (B / (1 - 2 ^ (-3 / (4 * ↑g)))) ^ (g * D.primeFactors.card)

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

theorem NairTenenbaum.badPrime_moment_exponent_gap {g η : ℕ} (hg : 0 < g) (hη : η ≤ g) {ε β : ℝ} (hεβ : 0 ≤ ε + β) (hsmall : ↑g ^ 2 * (ε + β) ≤ 1 / 4) : ↑η * (ε + β) - 1 / ↑g ≤ -3 / (4 * ↑g)

theorem NairTenenbaum.PolynomialSystem.badPrimeTupleKernel_moment_sum_le {k r : ℕ} (P : PolynomialSystem k r) {A B ε β : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (hg : 0 < P.total.natDegree) (hsmall : ↑P.total.natDegree ^ 2 * (ε + β) ≤ 1 / 4) (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 * ↑(weightedMass P.exponent n) ^ β ≤ badPrimeMomentBound B P.total.natDegree P.badDiscriminant

Every bad-prime valuation is included, with a constant independent of the cutoff and of the chosen small moment exponent.