Global exponential moments on smooth dagger tuples

The finite moment comparison retains the weighted-mass truncation, the finite prime support, and every dagger restriction. The resulting constant is uniform in the truncation and the smoothness cutoff. These are the root-weighted moment and Rankin steps of Lemma 2, before its final truncation argument.

theorem NairTenenbaum.weightedMass_rpow {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) (β : ℝ) : ↑(weightedMass γ n) ^ β = ∏ i : Fin r, ↑↑(n i) ^ (↑(totalExponent γ i) * β)

The real power of the weighted mass separates over the coordinates.

theorem NairTenenbaum.rootTupleWeight_moment_le_product {k r : ℕ} {A B ε β : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hβ : 0 ≤ β) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), ↑(totalExponent γ i) * (ε + β) < 1) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (D : ℕ) (s : Finset ℕ) (S : Finset (Tuple r)) (N : ℕ+) (hbox : ∀ n ∈ S, ∀ (i : Fin r), n i ≤ N) (hsmooth : ∀ n ∈ S, ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers s) (hdagger : ∀ n ∈ S, Dagger D n) (hrest : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, tupleUnitaryRest n t ∈ S) : ∑ n ∈ S, rootTupleWeight γ F Q n * ↑(weightedMass γ n) ^ β ≤ (∏ i : Fin r, ∏ p ∈ s with Nat.Prime p, (1 + localMomentError A B ε β (totalExponent γ i) (Q i) p)) * ∑ n ∈ S, rootTupleWeight γ F Q n

Moment comparison on any finite domain closed under unitary removal.

noncomputable def NairTenenbaum.smoothWeightUpTo {k r : ℕ} (γ : Fin k → Fin r → ℕ) (D : ℕ) (s : Finset ℕ) (N : ℕ+) : Finset (Tuple r)

Smooth tuples with a weighted-mass bound, retaining the full dagger condition.

Equations

• NairTenenbaum.smoothWeightUpTo γ D s N = {n ∈ NairTenenbaum.weightUpTo γ D N | ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers s}

theorem NairTenenbaum.mem_smoothWeightUpTo {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (s : Finset ℕ) (N : ℕ+) (n : Tuple r) : n ∈ smoothWeightUpTo γ D s N ↔ (weightedMass γ n ≤ ↑N ∧ Dagger D n) ∧ ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers s

theorem NairTenenbaum.tupleUnitaryRest_mem_smoothWeightUpTo {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (s : Finset ℕ) (N : ℕ+) {n : Tuple r} (hn : n ∈ smoothWeightUpTo γ D s N) (t : Fin r → Finset ℕ) : tupleUnitaryRest n t ∈ smoothWeightUpTo γ D s N

theorem NairTenenbaum.smoothWeightUpTo_moment_uniform {k r : ℕ} {A B ε κ σ z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hσ : σ < 1) (hz : 2 ≤ z) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hshift : ∀ (i : Fin r), ↑(totalExponent γ i) * (ε + κ / Real.log z) ≤ σ) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (D : ℕ) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight γ F Q n * ↑(weightedMass γ n) ^ (κ / Real.log z) ≤ (∏ i : Fin r, Real.exp (momentPrimeBound A B κ σ (totalExponent γ i) (C i))) * ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight γ F Q n

Global smooth moment estimate, uniform in both finite cutoffs.

theorem NairTenenbaum.sum_tail_le_moment {ι : Type u_1} (S : Finset ι) (w m : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (hm : ∀ (i : ι), 0 ≤ m i) {x β : ℝ} (hx : 0 < x) (hβ : 0 ≤ β) : ∑ i ∈ S with x < m i, w i ≤ x ^ (-β) * ∑ i ∈ S, w i * m i ^ β

Finite Rankin inequality, valid for every nonnegative weight.

theorem NairTenenbaum.sum_sum_tail_le_moment {ι : Type u_1} {υ : Type u_2} (V : Finset ι) (U : ι → Finset υ) (w m : ι → υ → ℝ) (hw : ∀ (v : ι) (u : υ), 0 ≤ w v u) (hm : ∀ (v : ι) (u : υ), 0 ≤ m v u) {x β : ℝ} (hx : 0 < x) (hβ : 0 ≤ β) : ∑ v ∈ V, ∑ u ∈ U v with x < m v u, w v u ≤ x ^ (-β) * ∑ v ∈ V, ∑ u ∈ U v, w v u * m v u ^ β

Rankin's inequality on a family of finite sets with a common mass cutoff.

theorem NairTenenbaum.sum_split_weightedMass_moment_le {k r : ℕ} (γ : Fin k → Fin r → ℕ) (V : Finset (Tuple r)) (U : Tuple r → Finset (Tuple r)) (w W : Tuple r → ℝ) {β B : ℝ} (hW : ∀ (v : Tuple r), 0 ≤ W v) (hlocal : ∀ v ∈ V, ∑ u ∈ U v, w u * ↑(weightedMass γ u) ^ β ≤ B) : ∑ v ∈ V, ∑ u ∈ U v, w u * W v * ↑(weightedMass γ (u * v)) ^ β ≤ B * ∑ v ∈ V, W v * ↑(weightedMass γ v) ^ β

Multiply a uniform moment bound for each bad part by the good-part moment.

theorem NairTenenbaum.smoothWeightUpTo_tail_uniform {k r : ℕ} {A B ε κ σ z x : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hσ : σ < 1) (hz : 2 ≤ z) (hx : 0 < x) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hshift : ∀ (i : Fin r), ↑(totalExponent γ i) * (ε + κ / Real.log z) ≤ σ) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (D : ℕ) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N with x < ↑(weightedMass γ n), rootTupleWeight γ F Q n ≤ Real.exp (-κ * Real.log x / Real.log z) * ((∏ i : Fin r, Real.exp (momentPrimeBound A B κ σ (totalExponent γ i) (C i))) * ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight γ F Q n)

The Rankin saving with the paper's logarithmic moment exponent.

theorem NairTenenbaum.PolynomialSystem.smooth_tail_bound {k r : ℕ} (P : PolynomialSystem k r) {A B ε κ z x : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hx : 0 < x) (hzκ : 4 ^ (↑P.total.natDegree * κ) ≤ z) (hεγ : ∀ (i : Fin r), ↑(totalExponent P.exponent i) * ε ≤ 1 / 8) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N with x < ↑(weightedMass P.exponent n), rootTupleWeight P.exponent F P.R n ≤ Real.exp (-κ * Real.log x / Real.log z) * ((∏ i : Fin r, Real.exp (momentPrimeBound A B κ (7 / 8) (totalExponent P.exponent i) (max (P.R i).natDegree (P.badDiscriminant ^ 3)))) * ∑ n ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight P.exponent F P.R n)

Actual polynomial systems satisfy the root-weighted smooth tail estimate with all root-count hypotheses discharged. The denominator still contains the full finite smooth sum, not the final n ≤ z truncation of Lemma 2.