Nonnegative weighted finite sieve for the existing external WF family

Indices are retained: entries may be zero or repeated, and no injectivity hypothesis is imposed. Only the nonnegative sequence weights multiply an inequality. The signed external coefficients are rearranged by exact finite sum identities. All divisor sums remain over the original primorial; no transport to a full level interval or analytic density estimate is claimed.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.weightedDivCount {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (d : ℕ) : ℝ

Weighted divisibility count on the original index set.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.weightedDivCount I a w d = ∑ i ∈ I, if d ∣ a i then w i else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.weightedSequenceSifted {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (P : Finset ℕ) : ℝ

Weighted sifted count, with index multiplicity preserved.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.weightedSequenceSifted I a w P = ∑ i ∈ I, w i * if (a i).Coprime (P.prod id) then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.weightedExternalUpper {ι : Type u_1} (P : Finset ℕ) (D ε z : ℝ) (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) : ℝ

The actual external upper family, applied to weighted counts.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.weightedExternalUpper P D ε z I a w = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D ε z t) d * MathlibNt.SieveTheory.LiLiuPrereqWF.weightedDivCount I a w d

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFamily_pointwise_upper (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε z : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) (n : ℕ) : (if n.Coprime (P.prod id) then 1 else 0) ≤ ∑ t ∈ externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (externalTerm true P D ε z t) d * if d ∣ n then 1 else 0

Singleton specialization of the existing external-family sieve. This includes the external edge range and the sequence value zero.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.weightedExternalUpper_eq_sum_points {ι : Type u_1} (P : Finset ℕ) (D ε z : ℝ) (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) : weightedExternalUpper P D ε z I a w = ∑ i ∈ I, w i * ∑ t ∈ externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (externalTerm true P D ε z t) d * if d ∣ a i then 1 else 0

Exact finite reordering; no sign assumptions on either weights or external coefficients are needed for this identity.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFamily_weighted_sequence_sieve {ι : Type u_1} (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε z : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (hw : ∀ i ∈ I, 0 ≤ w i) : (∑ i ∈ I, w i * if (a i).Coprime (P.prod id) then 1 else 0) ≤ ∑ t ∈ externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (externalTerm true P D ε z t) d * ∑ i ∈ I, if d ∣ a i then w i else 0

Nonnegative weighted upper sieve for arbitrary indexed natural numbers. Nonnegativity is required only on the finite index set.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.weightedExternalUpper_centering {ι : Type u_1} (P : Finset ℕ) (D ε z : ℝ) (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (H : ℕ → ℝ) : weightedExternalUpper P D ε z I a w = ∑ t ∈ externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (externalTerm true P D ε z t) d * H d + ∑ t ∈ externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (externalTerm true P D ε z t) d * (weightedDivCount I a w d - H d)

Exact centering about an arbitrary function H. This is finite ring algebra, with no primality, cutoff, positivity, or analytic assumptions.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFamily_weighted_sequence_sieve_centered {ι : Type u_1} (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε z : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (hw : ∀ i ∈ I, 0 ≤ w i) (H : ℕ → ℝ) : weightedSequenceSifted I a w P ≤ ∑ t ∈ externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (externalTerm true P D ε z t) d * H d + ∑ t ∈ externalTags true P D ε z, ∑ d ∈ (P.prod id).divisors, (externalTerm true P D ε z t) d * (weightedDivCount I a w d - H d)

The weighted sieve with its exact, arbitrarily centered signed error.