noncomputable def MathlibNt.SieveTheory.LiuWeight.liuBeta (N z y n : ℕ) : ℝ

The actual Liu weight convolved with the prime indicator.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuBeta N z y n = ∑ a ∈ n.divisors, MathlibNt.SieveTheory.LiuWeight.liuWeight N z y a * if Nat.Prime (n / a) then 1 else 0

def MathlibNt.SieveTheory.LiuWeight.liuBetaSupport (N z y n : ℕ) : Finset ℕ

Effective divisor terms, without multiplicities of pair representations.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuBetaSupport N z y n = {a ∈ n.divisors | MathlibNt.SieveTheory.LiuWeight.LiuWeightSupport N z y a ∧ Nat.Prime (n / a)}

theorem MathlibNt.SieveTheory.LiuWeight.liuBeta_eq_card (N z y n : ℕ) : liuBeta N z y n = ↑(liuBetaSupport N z y n).card

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuBeta_zero (N z y : ℕ) : liuBeta N z y 0 = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuBeta_nonneg (N z y n : ℕ) : 0 ≤ liuBeta N z y n

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaSupport_complement_injective (N z y n : ℕ) : Set.InjOn (fun (a : ℕ) => n / a) ↑(liuBetaSupport N z y n)

Distinct effective divisors have distinct complementary primes.

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaSupport_complement_mem_primeFactors {N z y n a : ℕ} (ha : a ∈ liuBetaSupport N z y n) : n / a ∈ n.primeFactors

Every effective complement belongs to the actual prime-factor carrier.

theorem MathlibNt.SieveTheory.LiuWeight.liuBetaSupport_card_le_three (N z y n : ℕ) : (liuBetaSupport N z y n).card ≤ 3

One effective term exhibits three prime factors; repetition only shrinks this three-element finite set.

theorem MathlibNt.SieveTheory.LiuWeight.liuBeta_le_three (N z y n : ℕ) : liuBeta N z y n ≤ 3

Uniform, including n=0, and requiring no squarefreeness.