def MathlibNt.SieveTheory.LiuWeight.liuAPCarrier (N q l : ℕ) : Finset ℕ

All nonnegative integers up to N in the specified residue class, not a prime-counting proxy. The residue need not be reduced or canonical.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuAPCarrier N q l = {n ∈ Finset.range (N + 1) | n ≡ l [MOD q]}

theorem MathlibNt.SieveTheory.LiuWeight.liuAPCarrier_card_le (N q l : ℕ) : (liuAPCarrier N q l).card ≤ N / q + 1

theorem MathlibNt.SieveTheory.LiuWeight.primesInAPBelow_eq_divisor_card (N a q l : ℕ) (ha : 0 < a) : AnalyticNumberTheory.Sieve.primesInAPBelow N a q l = {n ∈ liuAPCarrier N q l | a ∈ n.divisors ∧ Nat.Prime (n / a)}.card

Positive-a product-fibre bijection for the literal production prime count.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount (N z y A₁ A₂ q l : ℕ) : ℝ

Literal counting part of the source interval sum; no change to its Li term.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount N z y A₁ A₂ q l = ∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then MathlibNt.SieveTheory.LiuWeight.liuWeight N z y a * ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N a q l) else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuBetaInterval (N z y A₁ A₂ q n : ℕ) : ℝ

Product-fibre coefficient retaining both the interval and gcd restrictions.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuBetaInterval N z y A₁ A₂ q n = ∑ a ∈ n.divisors, if a ∈ Finset.Ioc A₁ A₂ ∧ a.Coprime q then MathlibNt.SieveTheory.LiuWeight.liuWeight N z y a * if Nat.Prime (n / a) then 1 else 0 else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount_eq_sum_betaInterval (N z y A₁ A₂ q l : ℕ) : liuCoprimeIntervalCount N z y A₁ A₂ q l = ∑ n ∈ liuAPCarrier N q l, liuBetaInterval N z y A₁ A₂ q n

Exact finite regrouping, valid without a reduced-residue assumption.

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaInterval_nonneg (N z y A₁ A₂ q n : ℕ) : 0 ≤ liuBetaInterval N z y A₁ A₂ q n

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaInterval_le_beta (N z y A₁ A₂ q n : ℕ) : liuBetaInterval N z y A₁ A₂ q n ≤ liuBeta N z y n

Removing nonnegative interval/gcd filters can only increase a fibre.

theorem MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount_le_three_mul_div_add_one (N z y A₁ A₂ q l : ℕ) : liuCoprimeIntervalCount N z y A₁ A₂ q l ≤ 3 * (↑(N / q) + 1)

Whole-a counting bound: no termwise error triangle inequality.

theorem MathlibNt.SieveTheory.LiuWeight.liuCoprimeIntervalCount_le_three_mul_real_div_add_one (N z y A₁ A₂ q l : ℕ) (hq : 0 < q) : liuCoprimeIntervalCount N z y A₁ A₂ q l ≤ 3 * (↑N / ↑q + 1)

Real-division form, for every positive modulus and arbitrary residue.