Comparing the sifting product at two power-related cutoffs

theorem NairTenenbaum.sieveProduct_cutoff_identity {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {w z : ℝ} (hw : 0 ≤ w) (hwz : w ≤ z) : sieveProduct Q w = sieveProduct Q z * ∏ p ∈ primeBandNumbers w z with Nat.Prime p, (1 - ↑(rootCount Q p) / ↑p)⁻¹

Exact restoration of the factors between two cutoffs.

theorem NairTenenbaum.sieveProduct_cutoff_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g : ℕ} (hg : Q.natDegree ≤ g) {w z : ℝ} (hw : 2 ≤ w) (hwz : w ≤ z) (hgw : 2 * ↑g ≤ w) : sieveProduct Q w ≤ sieveProduct Q z * Real.exp (2 * ↑g * (Real.log 4 * (1 + Real.log z) / Real.log w))

A coefficient-independent comparison in terms of the logarithm ratio.

theorem NairTenenbaum.sieveProduct_power_cutoff_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {g : ℕ} (hg : Q.natDegree ≤ g) {α x : ℝ} (hα : 0 < α) (hα₁ : α ≤ 1) (hx : 1 ≤ x) (hlog : 1 ≤ Real.log x) (hw : 2 ≤ x ^ α) (hgw : 2 * ↑g ≤ x ^ α) : sieveProduct Q (x ^ α) ≤ Real.exp (4 * ↑g * Real.log 4 / α) * sieveProduct Q x

At w=x^α, the comparison costs a constant depending only on degree and α, once the smaller cutoff exceeds 2g and log x≥1.

theorem NairTenenbaum.exists_sieveProduct_power_cutoff_bound (g : ℕ) {α : ℝ} (hα : 0 < α) (hα₁ : α ≤ 1) : ∃ (x₀ : ℝ), 1 ≤ x₀ ∧ ∀ (x : ℝ), x₀ ≤ x → ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → Q.natDegree ≤ g → sieveProduct Q (x ^ α) ≤ Real.exp (4 * ↑g * Real.log 4 / α) * sieveProduct Q x

Uniform threshold for the power-cutoff comparison.