Divisor-window tail saving in the presence of fixed prime divisors

theorem NairTenenbaum.exists_polynomialDivisorLargeSum_power_saving_unrestricted {Q : Polynomial ℤ} (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {α η : ℝ} (hα : 0 < α) (hη : Real.log 4 - 1 < η) : ∃ (δ : ℝ) (x₀ : ℝ) (C : ℝ), 0 < δ ∧ 1 < x₀ ∧ 0 < C ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x / 2 → polynomialDivisorLargeSum Q η x y ≤ C * y * Real.log x ^ (-δ)

theorem NairTenenbaum.exists_polynomialDivisorLargeSum_small_unrestricted {Q : Polynomial ℤ} (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {α η c : ℝ} (hα : 0 < α) (hη : Real.log 4 - 1 < η) (hc : 0 < c) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x / 2 → polynomialDivisorLargeSum Q η x y ≤ c * y

theorem NairTenenbaum.exists_polynomialDivisorWindowSum_le_hits_add_small_unrestricted {Q : Polynomial ℤ} (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {α η c : ℝ} (hα : 0 < α) (hη : Real.log 4 - 1 < η) (hc : 0 < c) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x / 2 → polynomialDivisorWindowSum Q x y ≤ Real.log x ^ η * ↑(polynomialDivisorHitCount Q x y) + c * y