Absorbing the smooth tail

The smaller smoothness cutoff is chosen so that the moment bound makes its tail at most half of the full sum. The prime-band comparison then reduces the original smooth sum to a sum with weighted mass at most z.

noncomputable def NairTenenbaum.smoothTruncationScale {k r : ℕ} (A B : ℝ) (γ : Fin k → Fin r → ℕ) (C : Fin r → ℕ) : ℝ

An explicit constant for choosing the smaller smoothness cutoff.

Equations

• NairTenenbaum.smoothTruncationScale A B γ C = 1 + |∑ i : Fin r, NairTenenbaum.momentPrimeBound A B 1 (7 / 8) (NairTenenbaum.totalExponent γ i) (C i)| + Real.log 2

theorem NairTenenbaum.smoothTruncationScale_one_le {k r : ℕ} (A B : ℝ) (γ : Fin k → Fin r → ℕ) (C : Fin r → ℕ) : 1 ≤ smoothTruncationScale A B γ C

theorem NairTenenbaum.smoothTruncationScale_absorb {k r : ℕ} (A B : ℝ) (γ : Fin k → Fin r → ℕ) (C : Fin r → ℕ) : Real.exp (-smoothTruncationScale A B γ C) * ∏ i : Fin r, Real.exp (momentPrimeBound A B 1 (7 / 8) (totalExponent γ i) (C i)) ≤ 1 / 2

This choice of scale makes the moment correction times the Rankin saving at most one half. No sign assumption on the written correction constant is needed.

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

The finite absorption step. Its hypotheses expose exactly what is required of the smaller cutoff; the following theorem supplies it explicitly.

theorem NairTenenbaum.smoothWeightUpTo_truncation_large {k r : ℕ} {A B ε z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε ≤ 1 / 8) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (G : ℕ) (hG : ∀ (i : Fin r), totalExponent γ i ≤ G) (hz : max 2 (4 ^ G) ^ smoothTruncationScale A B γ C ≤ z) (D : ℕ) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight γ F Q n ≤ (2 * ∏ i : Fin r, primeBandBound A B (1 / 8) (smoothTruncationScale A B γ C) (totalExponent γ i) (C i)) * ∑ n ∈ weightUpTo γ D N with ↑(weightedMass γ n) ≤ z, rootTupleWeight γ F Q n

A fixed large-cutoff threshold supplies the smaller smoothness cutoff. The bound is uniform in the mass cutoff and the arithmetic function.