Uniform truncation for every smoothness cutoff

The large-cutoff absorption argument is supplemented by a fixed Euler product for the bounded range. The resulting constant is independent of both cutoffs, the arithmetic function, and the polynomial coefficients apart from their supplied uniform root bounds.

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

Uniform bound for a whole local auxiliary series.

theorem NairTenenbaum.rootTupleWeight_sum_le_euler {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (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) (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) : ∑ n ∈ S, rootTupleWeight γ F Q n ≤ F 1 * ∏ i : Fin r, ∏ p ∈ s with Nat.Prime p, ∑' (ν : ℕ), rootAuxiliary A B ε (totalExponent γ i) (Q i) (p ^ ν)

A finite smooth tuple sum is bounded by its coordinate auxiliary products.

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

The uniform threshold for comparing the two smooth-weight cutoffs.

Equations

• NairTenenbaum.smoothTruncationThreshold A B γ C G = max 2 (4 ^ G) ^ NairTenenbaum.smoothTruncationScale A B γ C

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

The constant in the uniform smooth-weight truncation comparison.

Equations

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

theorem NairTenenbaum.smoothTruncationBound_pos {k r : ℕ} {A B : ℝ} (hB : 0 ≤ B) (γ : Fin k → Fin r → ℕ) (C : Fin r → ℕ) (G : ℕ) : 0 < smoothTruncationBound A B γ C G

theorem NairTenenbaum.one_le_truncated_rootTupleWeight_sum {k r : ℕ} {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (Q : Fin r → Polynomial ℤ) (D : ℕ) (N : ℕ+) {z : ℝ} (hz : 1 ≤ z) : F 1 ≤ ∑ n ∈ weightUpTo γ D N with ↑(weightedMass γ n) ≤ z, rootTupleWeight γ F Q n

The tuple 1 contributes F(1) to every nonempty mass truncation.

theorem NairTenenbaum.smoothWeightUpTo_truncation_uniform {k r : ℕ} {A B ε z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hz : 2 ≤ z) (γ : 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) (D : ℕ) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight γ F Q n ≤ smoothTruncationBound A B γ C G * ∑ n ∈ weightUpTo γ D N with ↑(weightedMass γ n) ≤ z, rootTupleWeight γ F Q n

Uniform finite smooth truncation for every z ≥ 2.