Fixed piecewise families at the external edge

Above sqrt D the lower family is a singleton zero weight and the upper family is the original family on primes below sqrt D. No coefficients are masked. Both the density and the signed remainder below sum the actual members over divisors of the ORIGINAL primorial.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalEdgePrimes (P : Finset ℕ) (D : ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalEdgePrimes P D = {p ∈ P | ↑p < √D}

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) : Finset (List ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags upper P D ε z = if z ≤ √D then MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags upper P D ε (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel D ε) else if upper = true then MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags true (MathlibNt.SieveTheory.LiLiuPrereqWF.externalEdgePrimes P D) D ε (MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSieveLabel D ε) else {[]}

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (t : List ℕ) : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm upper P D ε z t = if z ≤ √D then MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm upper P D ε t else if upper = true then MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm true (MathlibNt.SieveTheory.LiLiuPrereqWF.externalEdgePrimes P D) D ε t else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalDensity (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (g : ArithmeticFunction ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalDensity upper P D ε z g = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags upper P D ε z, ∑ d ∈ (P.prod id).divisors, (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm upper P D ε z t) d * g d

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.externalRemainder {ι : Type u_1} (upper : Bool) (P : Finset ℕ) (D ε z : ℝ) (I : Finset ι) (a : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.externalRemainder upper P D ε z I a X g = ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags upper P D ε z, ∑ d ∈ (P.prod id).divisors, (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm upper P D ε z t) d * MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder I a X g d

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceSifted_nonneg {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) (P : Finset ℕ) : 0 ≤ sequenceSifted I a P

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceSifted_antitone {ι : Type u_1} (I : Finset ι) (a : ι → ℕ) {B P : Finset ℕ} (hBP : B ⊆ P) : sequenceSifted I a P ≤ sequenceSifted I a B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_sum_subcarrier (upper : Bool) {B P : Finset ℕ} (hBP : B ⊆ P) (hP : ∀ p ∈ P, Nat.Prime p) (D ε : ℝ) (t : List ℕ) (r : ℕ → ℝ) : ∑ d ∈ (P.prod id).divisors, (signedFamilyTerm upper B D ε t) d * r d = ∑ d ∈ (B.prod id).divisors, (signedFamilyTerm upper B D ε t) d * r d

Enlarging only the summation carrier does not change these coefficients on squarefree divisors; their non-squarefree extension remains untouched.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyDensity_eq_member_sum (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (g : ArithmeticFunction ℝ) : signedFamilyDensity upper P D ε label g = ∑ t ∈ signedTags upper P D ε label, ∑ d ∈ (P.prod id).divisors, (signedFamilyTerm upper P D ε t) d * g d

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalDensity_eq (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (D ε z : ℝ) (g : ArithmeticFunction ℝ) : externalDensity upper P D ε z g = if z ≤ √D then signedFamilyDensity upper P D ε (geometricSieveLabel D ε) g else if upper = true then signedFamilyDensity true (externalEdgePrimes P D) D ε (geometricSieveLabel D ε) g else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalRemainder_eq {ι : Type u_1} (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (D ε z : ℝ) (I : Finset ι) (a : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : externalRemainder upper P D ε z I a X g = if z ≤ √D then signedFamilyRemainder upper P D ε (geometricSieveLabel D ε) I a X g else if upper = true then signedFamilyRemainder true (externalEdgePrimes P D) D ε (geometricSieveLabel D ε) I a X g else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.zero_wellFactorable {Q : ℝ} (hQ : 1 ≤ Q) : WellFactorable 0 Q

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags_card_and_wellFactorable (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (z : ℝ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) : ↑(externalTags upper P D ε z).card < Real.exp (8 * ε⁻¹ ^ 3) ∧ ∀ t ∈ externalTags upper P D ε z, WellFactorable (externalTerm upper P D ε z t) (D ^ (1 + ε + ε ^ 9))

These exact families, including the singleton zero lower edge, satisfy the original source cardinality bound before all level splits.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFamily_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 : ι → ℕ) (X : ℝ) (g : ArithmeticFunction ℝ) : X * externalDensity false P D ε z g + externalRemainder false P D ε z I a X g ≤ sequenceSifted I a P ∧ sequenceSifted I a P ≤ X * externalDensity true P D ε z g + externalRemainder true P D ε z I a X g

Finite sieve direction for the actual piecewise families. In the edge range the upper inequality is sieve monotonicity and the lower is positivity. Analytic F/f density is a separate obligation.