Uniform prime bounds for exponential moments

The first-power terms use the logarithmic prime estimate. Higher powers are controlled geometrically: a fixed finite set of small primes uses the growth exponent, and large primes use the sharper A^γ/p ratio.

theorem NairTenenbaum.localMoment_tail_le {A B ε β M q : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hβ : 0 ≤ β) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (hq₀ : 0 ≤ q) (hq₁ : q < 1) (hbound : ∀ (ν : ℕ), tiltedRootAuxiliary A B ε β γ Q (p ^ ν) ≤ M * q ^ ν) (N : ℕ) : ∑' (ν : ℕ), localMomentTerm A B ε β γ Q p (ν + N) ≤ M * q ^ (N + 1) / (1 - q)

A geometric majorant controls every tail of the local moment increment.

theorem NairTenenbaum.localMoment_higher_le_small {A B ε β σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (hσ : σ < 1) (γ : ℕ) (hγ : ↑γ * (ε + β) ≤ σ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∑' (ν : ℕ), localMomentTerm A B ε β γ Q p (ν + 1) ≤ ↑C * B / (1 - 2 ^ (σ - 1))

A prime-independent bound from a fixed gap below the convergence exponent.

theorem NairTenenbaum.localMoment_higher_le_large {A B ε β K : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (γ : ℕ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (hK : 0 ≤ K) (hpow : A ^ γ * ↑p ^ (↑γ * β) ≤ K) (hpK : 2 * K ≤ ↑p) : ∑' (ν : ℕ), localMomentTerm A B ε β γ Q p (ν + 1) ≤ 2 * ↑C * B * K ^ 2 / ↑p ^ 2

At large primes the higher-power tail has a summable inverse-square bound.

noncomputable def NairTenenbaum.momentHigherMajorant (B σ K : ℝ) (C n : ℕ) : ℝ

A cutoff-independent majorant for the higher-power tail.

Equations

• NairTenenbaum.momentHigherMajorant B σ K C n = (if n ≤ ⌈2 * K⌉₊ then ↑C * B / (1 - 2 ^ (σ - 1)) else 0) + 2 * ↑C * B * K ^ 2 * ↑n ^ (-2)

theorem NairTenenbaum.momentHigherMajorant_nonneg {B σ K : ℝ} (hB : 0 ≤ B) (hσ : σ < 1) (C n : ℕ) : 0 ≤ momentHigherMajorant B σ K C n

theorem NairTenenbaum.momentHigherMajorant_summable (B σ K : ℝ) (C : ℕ) : Summable (momentHigherMajorant B σ K C)

theorem NairTenenbaum.rpow_log_cutoff_le_exp {z κ : ℝ} (hz : 2 ≤ z) (hκ : 0 ≤ κ) (γ : ℕ) {p : ℕ} (hp : Nat.Prime p) (hpz : ↑p ≤ z) : ↑p ^ (↑γ * (κ / Real.log z)) ≤ Real.exp (↑γ * κ)

The varying exponent is uniformly bounded at all primes below the cutoff.

theorem NairTenenbaum.localMoment_higher_le_majorant {A B ε κ σ z : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hσ : σ < 1) (hz : 2 ≤ z) (γ : ℕ) (hγ : ↑γ * (ε + κ / Real.log z) ≤ σ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (hpz : ↑p ≤ z) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∑' (ν : ℕ), localMomentTerm A B ε (κ / Real.log z) γ Q p (ν + 1) ≤ momentHigherMajorant B σ (A ^ γ * Real.exp (↑γ * κ)) C p

The full higher-power tail is bounded by one fixed summable sequence.

noncomputable def NairTenenbaum.momentPrimeBound (A B κ σ : ℝ) (γ C : ℕ) : ℝ

An explicit bound independent of the cutoff and polynomial coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.localMomentError_sum_uniform {A B ε κ σ z : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hσ : σ < 1) (hz : 2 ≤ z) (γ : ℕ) (hγ : ↑γ * (ε + κ / Real.log z) ≤ σ) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∑ p ∈ Finset.Icc 0 ⌊z⌋₊ with Nat.Prime p, localMomentError A B ε (κ / Real.log z) γ Q p ≤ momentPrimeBound A B κ σ γ C

The complete local-error sum is bounded uniformly in z, provided the tilted exponent stays a fixed distance below one.

theorem NairTenenbaum.localMomentError_product_uniform {A B ε κ σ z : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hσ : σ < 1) (hz : 2 ≤ z) (γ : ℕ) (hγ : ↑γ * (ε + κ / Real.log z) ≤ σ) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∏ p ∈ Finset.Icc 0 ⌊z⌋₊ with Nat.Prime p, (1 + localMomentError A B ε (κ / Real.log z) γ Q p) ≤ Real.exp (momentPrimeBound A B κ σ γ C)

The moment correction Euler product is uniform in the smoothness cutoff.

theorem NairTenenbaum.moment_exponent_gap {ε κ z : ℝ} (γ : ℕ) (hεγ : ↑γ * ε ≤ 1 / 8) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hzκ : 4 ^ (↑γ * κ) ≤ z) : ↑γ * (ε + κ / Real.log z) ≤ 7 / 8

The logarithmic choice of exponent stays uniformly below one at the paper's exponential smoothness threshold.

theorem NairTenenbaum.PolynomialSystem.factor_moment_product_bound {k r : ℕ} (P : PolynomialSystem k r) {A B ε κ z : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hzκ : 4 ^ (↑P.total.natDegree * κ) ≤ z) (h : Fin r) (hεγ : ↑(totalExponent P.exponent h) * ε ≤ 1 / 8) : ∏ p ∈ Finset.Icc 0 ⌊z⌋₊ with Nat.Prime p, (1 + localMomentError A B ε (κ / Real.log z) (totalExponent P.exponent h) (P.R h) p) ≤ Real.exp (momentPrimeBound A B κ (7 / 8) (totalExponent P.exponent h) (max (P.R h).natDegree (P.badDiscriminant ^ 3)))

The uniform exponential-moment product for each actual polynomial factor. All root-count assumptions are discharged by the proved discriminant bounds.