Documentation

MathlibNt.SieveTheory.Distribution.LiuPan.LiuPanLiMainTermEnvelope

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

source
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.

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

The fixed coefficient costs only the lower endpoint log 2.

Equations
Instances For
    source
    theorem MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant_pos (κ : ℝ) :
    0 < liuPanLiEnvelopeConstant κ
    source
    theorem MathlibNt.SieveTheory.LiuWeight.liuPanLiEnvelopeConstant_nonneg (κ : ℝ) :
    0 ≤ liuPanLiEnvelopeConstant κ
    source
    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.

    source
    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.

    source
    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.

    source
    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₂.

    source
    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.

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

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

    Equations
    Instances For
      source
      theorem MathlibNt.SieveTheory.LiuWeight.liuPanLiModulusEnvelopeConstant_pos (κ : ℝ) :
      0 < liuPanLiModulusEnvelopeConstant κ
      source
      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.

      source
      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₂.

      source
      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.