Comparison of two smoothness cutoffs

Splitting off all primes above the smaller cutoff is injective. The dagger conditions supply the cross-coprimality needed by the arithmetic majorant, and the removed part is bounded by the prime-band Euler product.

theorem NairTenenbaum.sum_positive_factored_le_tsum {f : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (s : Finset ℕ) (hs : Summable fun (n : ↑(Nat.factoredNumbers s)) => f ↑n) (T : Finset ℕ+) (hT : ∀ n ∈ T, ↑n ∈ Nat.factoredNumbers s) : ∑ n ∈ T, f ↑n ≤ ∑' (n : ↑(Nat.factoredNumbers s)), f ↑n

A finite positive-integer sum embeds in the corresponding smooth series.

theorem NairTenenbaum.rootAuxiliary_sum_le_product {A B ε : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) (hγ : ↑γ * ε < 1) (Q : Polynomial ℤ) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) (s : Finset ℕ) (T : Finset ℕ+) (hT : ∀ n ∈ T, ↑n ∈ Nat.factoredNumbers s) : ∑ n ∈ T, rootAuxiliary A B ε γ Q ↑n ≤ ∏ p ∈ s with Nat.Prime p, ∑' (ν : ℕ), rootAuxiliary A B ε γ Q (p ^ ν)

theorem NairTenenbaum.weightedMass_unitaryPart_le {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) (t : Fin r → Finset ℕ) : weightedMass γ (tupleUnitaryPart n t) ≤ weightedMass γ n

theorem NairTenenbaum.unitaryPart_mem_factoredNumbers (n : ℕ+) (s : Finset ℕ) : ↑(unitaryPart n s) ∈ Nat.factoredNumbers s

Selecting primes in a set always produces an integer factored over that set.

theorem NairTenenbaum.unitaryRest_mem_primeBand {w z : ℝ} (hw : 0 ≤ w) {n : ℕ+} (hn : ↑n ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊)) : ↑(unitaryRest n (Finset.Icc 0 ⌊w⌋₊)) ∈ Nat.factoredNumbers (primeBandNumbers w z)

The complement to the smaller smooth part has every prime in the band.

theorem NairTenenbaum.smoothWeightUpTo_cutoff_le_product {k r : ℕ} {A B ε w z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hw : 0 ≤ w) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (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 : ℕ) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight γ F Q n ≤ (∏ i : Fin r, ∏ p ∈ primeBandNumbers w z with Nat.Prime p, ∑' (ν : ℕ), rootAuxiliary A B ε (totalExponent γ i) (Q i) (p ^ ν)) * ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊w⌋₊) N, rootTupleWeight γ F Q n

Shrinking the smoothness cutoff costs only the Euler product over the removed band. The finite weighted-mass bound remains unchanged.

theorem NairTenenbaum.smoothWeightUpTo_cutoff_uniform {k r : ℕ} {A B ε σ L w z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1 / 2) (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) * ε ≤ σ) (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 ≤ (∏ i : Fin r, primeBandBound A B σ L (totalExponent γ i) (C i)) * ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊w⌋₊) N, rootTupleWeight γ F Q n

A uniform comparison between two smoothness cutoffs with bounded logarithm ratio, including the weighted-mass bound and all dagger restrictions.