Absorbing a power saving into the main term

theorem NairTenenbaum.PolynomialSystem.value_one_le_weight_one {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) : F 1 ≤ P.weight F 1

The unit tuple is always an admissible term in the weight at one.

theorem NairTenenbaum.PolynomialSystem.value_one_le_weight_sum {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) {x : ℝ} (hx : 1 ≤ x) : F 1 ≤ ∑ n ∈ positiveUpTo x, P.weight F n

theorem NairTenenbaum.exists_rpow_neg_le_sieveProduct (g : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → Q.natDegree ≤ g → ∀ (x : ℝ), 2 ≤ x → x ^ (-δ) ≤ C * sieveProduct Q x

The inverse sieve estimate is equivalently a lower bound by every fixed negative power, uniformly in the coefficients.

theorem NairTenenbaum.exists_powerSaving_le_mainTerm (g : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree ≤ g → ∀ (F : ArithmeticMap k), (∀ (n : Tuple k), 0 ≤ F n) → ∀ (x y : ℝ), 2 ≤ x → 0 ≤ y → y * x ^ (-δ) * F 1 ≤ C * mainTerm P F x y

A power-saving error times F(1) is dominated by the full main term, without a normalization assumption on the arithmetic function.