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

Equations

• MathlibNt.SieveTheory.LiuWeight.liuActualEnvelopeConstant κ = 6 + MathlibNt.SieveTheory.LiuWeight.liuPanLiModulusEnvelopeConstant κ

theorem MathlibNt.SieveTheory.LiuWeight.liuActualEnvelopeConstant_pos (κ : ℝ) : 0 < liuActualEnvelopeConstant κ

theorem MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount_nonneg (N z y A₁ A₂ q l : ℕ) : 0 ≤ liuCoprimeIntervalCount N z y A₁ A₂ q l

theorem MathlibNt.SieveTheory.LiuWeight.modulus_mul_liuCoprimeIntervalCount_le (N z y A₁ A₂ q l : ℕ) (hq : 0 < q) (hqN : q ≤ N) : ↑q * liuCoprimeIntervalCount N z y A₁ A₂ q l ≤ 6 * ↑N

theorem MathlibNt.SieveTheory.LiuWeight.modulus_mul_abs_liuMainPanCoprimeIntervalSum_le (κ : ℝ) (N A₁ A₂ q l : ℕ) (hN : 2 ≤ N) (hq : 0 < q) (hqN : q ≤ N) : ↑q * |liuMainPanCoprimeIntervalSum (liuLogarithmicIntegral κ) N A₁ A₂ q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))| ≤ liuActualEnvelopeConstant κ * ↑N * (1 + Real.log ↑N) ^ 2

Literal whole-error envelope, uniform over every interval and residue.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL_nonneg (main : ℝ → ℝ) (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) : 0 ≤ liuMainPanCoprimeIntervalMaxL main N A₁ A₂ q f

theorem MathlibNt.SieveTheory.LiuWeight.modulus_mul_liuMainPanCoprimeIntervalMaxL_le (κ : ℝ) (N A₁ A₂ q : ℕ) (hN : 2 ≤ N) (hq : 0 < q) (hqN : q ≤ N) : ↑q * liuMainPanCoprimeIntervalMaxL (liuLogarithmicIntegral κ) N A₁ A₂ q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ liuActualEnvelopeConstant κ * ↑N * (1 + Real.log ↑N) ^ 2

The actual reduced-residue maximum, including q=1, with a fixed κ constant.