Pointwise envelopes for the literal Liu main term. The additive normalization κ is unrestricted; no distribution hypothesis is introduced.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_ne_zero_index_and_quotient {N z y a : ℕ} (ha : liuWeight N z y a ≠ 0) : 1 ≤ a ∧ a ≤ N ∧ 2 ≤ ↑N / ↑a

Nonzero Liu weight forces a positive supported index and a real quotient ≥ 2.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant (κ : ℝ) : ℝ

The fixed coefficient costs only the lower endpoint log 2.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant κ = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegralUpperConstant κ / Real.log 2

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant_pos (κ : ℝ) : 0 < liuPanLiEnvelopeConstant κ

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant_nonneg (κ : ℝ) : 0 ≤ liuPanLiEnvelopeConstant κ

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuWeight_mul_logarithmicIntegral_le (κ : ℝ) (N z y a : ℕ) : |liuWeight N z y a * liuLogarithmicIntegral κ (↑N / ↑a)| ≤ liuPanLiEnvelopeConstant κ * ↑N * (liuWeight N z y a / ↑a)

The genuine integral is evaluated only on its supported domain.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_div_finset_le_one_add_log (N : ℕ) (S : Finset ℕ) : ∑ a ∈ S, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a / ↑a ≤ 1 + Real.log ↑N

Any finite window can be enlarged to the mother sum, even above N.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanLi_mainTerm_finset_le (κ : ℝ) (N q : ℕ) (S : Finset ℕ) : |∑ a ∈ S, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuLogarithmicIntegral κ (↑N / ↑a) / ↑q.totient| ≤ liuPanLiEnvelopeConstant κ * ↑N * (1 + Real.log ↑N) / ↑q.totient

Whole-sum absolute value, literal genuine Liκ, and original totient divisor.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanLi_mainTerm_Ioc_le (κ : ℝ) (N q A₁ A₂ : ℕ) : |∑ a ∈ Finset.Ioc A₁ A₂ with a.Coprime q, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuLogarithmicIntegral κ (↑N / ↑a) / ↑q.totient| ≤ liuPanLiEnvelopeConstant κ * ↑N * (1 + Real.log ↑N) / ↑q.totient

Uniform interval version, with no upper restriction on A₂.

theorem MathlibNt.SieveTheory.LiuWeight.exists_abs_liuPanLi_mainTerm_Ioc_le (κ : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N q A₁ A₂ : ℕ), 2 ≤ N → 0 < q → |∑ a ∈ Finset.Ioc A₁ A₂ with a.Coprime q, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuLogarithmicIntegral κ (↑N / ↑a) / ↑q.totient| ≤ C * ↑N * (1 + Real.log ↑N) / ↑q.totient

The constant is selected before all endpoints and moduli.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLiModulusEnvelopeConstant (κ : ℝ) : ℝ

The extra reciprocal-totient payment is independent of N, q and the window.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLiModulusEnvelopeConstant κ = MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant κ * MathlibNt.SieveTheory.Richert1969.richertReciprocalTotientConstant

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLiModulusEnvelopeConstant_pos (κ : ℝ) : 0 < liuPanLiModulusEnvelopeConstant κ

theorem MathlibNt.SieveTheory.LiuWeight.modulus_mul_abs_liuPanLi_mainTerm_finset_le (κ : ℝ) {N q : ℕ} (hN : 2 ≤ N) (hq : 0 < q) (hqN : q ≤ N) (S : Finset ℕ) : ↑q * |∑ a ∈ S, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuLogarithmicIntegral κ (↑N / ↑a) / ↑q.totient| ≤ liuPanLiModulusEnvelopeConstant κ * ↑N * (1 + Real.log ↑N) ^ 2

Multiplication by q costs at most a second logarithm for 0 < q ≤ N.

theorem MathlibNt.SieveTheory.LiuWeight.modulus_mul_abs_liuPanLi_mainTerm_Ioc_le (κ : ℝ) {N q : ℕ} (hN : 2 ≤ N) (hq : 0 < q) (hqN : q ≤ N) (A₁ A₂ : ℕ) : ↑q * |∑ a ∈ Finset.Ioc A₁ A₂ with a.Coprime q, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuLogarithmicIntegral κ (↑N / ↑a) / ↑q.totient| ≤ liuPanLiModulusEnvelopeConstant κ * ↑N * (1 + Real.log ↑N) ^ 2

Coprime interval specialization, still with no upper restriction on A₂.

theorem MathlibNt.SieveTheory.LiuWeight.exists_modulus_mul_abs_liuPanLi_mainTerm_Ioc_le (κ : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N q A₁ A₂ : ℕ), 2 ≤ N → 0 < q → q ≤ N → ↑q * |∑ a ∈ Finset.Ioc A₁ A₂ with a.Coprime q, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuLogarithmicIntegral κ (↑N / ↑a) / ↑q.totient| ≤ C * ↑N * (1 + Real.log ↑N) ^ 2

Quantifier order suitable for the later actual interval-maximal error bound.