Same-family density and the small-weight replacement cost

All densities below belong to the fixed normalized family of SignedFamily. The negative rough mass is counted once per prime subset, not once per labelled permutation. The upper replacement error is added, and the lower replacement error is subtracted. The remaining coarse rounded density is not estimated by the small-weight fundamental lemma.

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

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.smallWeightDensity upper P D ε g = ∑ d ∈ ((MathlibNt.SieveTheory.LiLiuPrereqWF.geometricSmallPrimes P D ε).prod id).divisors, (if upper = true then (MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight P D ε) d else (MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight P D ε) d) * g d

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyDensity (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (label : ℕ → ℕ) (g : ArithmeticFunction ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyDensity upper P D ε label g = ∑ d ∈ (P.prod id).divisors, (MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyAggregate upper P D ε label) d * g d

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.roughSignedDensity upper b c D R g = ∑ r ∈ R.powerset, MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet upper b c D r * ∏ p ∈ r, g p

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.negativeRoughMass (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) : ℝ

The magnitude of the actual odd (negative) coefficient, not an absolute value bound on a different box expansion.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.negativeRoughMass upper b c D R g = ∑ r ∈ R.powerset, (if Even r.card then 0 else -MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedSignedSet upper b c D r) * ∏ p ∈ r, g p

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyDensity_partition (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) (hhead : ∀ p ∈ P \ geometricSmallPrimes P D ε, geometricLower D ε (ε ^ 9) (label p) ^ 2 < D) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : signedFamilyDensity upper P D ε label g = ∑ r ∈ (P \ geometricSmallPrimes P D ε).powerset, (normalizedSignedSet upper (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p)) (fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p) ^ (1 + ε ^ 9)) D r * if LooseSign upper r.card then smallWeightDensity true P D ε g else smallWeightDensity false P D ε g) * ∏ p ∈ r, g p

Exact multiplicative-density reindexing of the actual full-integer aggregate on its squarefree consumption domain.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyDensity_replacement_identity (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hlabel : ∀ p ∈ P \ geometricSmallPrimes P D ε, p ∈ geometricPrimeBox P D ε (ε ^ 9) (label p)) (hhead : ∀ p ∈ P \ geometricSmallPrimes P D ε, geometricLower D ε (ε ^ 9) (label p) ^ 2 < D) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : have B := geometricSmallPrimes P D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p); have c := fun (p : ℕ) => b p ^ (1 + ε ^ 9); signedFamilyDensity upper P D ε label g = smallWeightDensity upper P D ε g * roughSignedDensity upper b c D (P \ B) ⇑g + (if upper = true then 1 else -1) * (smallWeightDensity true P D ε g - smallWeightDensity false P D ε g) * negativeRoughMass upper b c D (P \ B) ⇑g

Both signs use the SAME aggregate: the upper error is positive and the lower error negative when hi ≥ lo.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.negativeRoughMass_bounds (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (R : Finset ℕ) (g : ℕ → ℝ) (hg : ∀ p ∈ R, 0 ≤ g p) : 0 ≤ negativeRoughMass upper b c D R g ∧ negativeRoughMass upper b c D R g ≤ ∏ p ∈ R, (1 + g p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_signedFamilyDensity_replacement_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 2 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → (∀ p ∈ P \ geometricSmallPrimes P D ε, ↑p < √D) → ∀ (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ P, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity ω)) K → ∀ (upper : Bool), have B := geometricSmallPrimes P D ε; have label := geometricSieveLabel D ε; have b := fun (p : ℕ) => geometricLower D ε (ε ^ 9) (label p); have c := fun (p : ℕ) => b p ^ (1 + ε ^ 9); have V := ∏ p ∈ B, (1 - ω p / ↑p); have E := C * (Real.exp (-(1 / ε)) + Real.exp (√K - 1 / ε) * (ε * Real.log D) ^ (-(1 / 3))); have δ := signedFamilyDensity upper P D ε label (SmallRosser.primeDensity ω) - smallWeightDensity upper P D ε (SmallRosser.primeDensity ω) * roughSignedDensity upper b c D (P \ B) ⇑(SmallRosser.primeDensity ω); 0 ≤ (if upper = true then 1 else -1) * δ ∧ |δ| ≤ 2 * V * E * ∏ p ∈ P \ B, (1 + ω p / ↑p)

The accepted full small-weight fundamental lemma now pays the replacement inside this very family. The absolute constant precedes epsilon, and the large-D threshold precedes P, omega, K and the choice of side.

The rough Euler majorant is explicit; this is NOT the remaining estimate of the signed rounded density by the linear-sieve functions F and f.