Exact density defects for the actual small Rosser weights

The finite starting point for Iwaniec (1980), p.316 (22). The boundary is a failed cubic test at the newly inserted least prime, with equality on the failure side. The lower error is subtracted and the upper error is added. No analytic estimate for these explicit errors is assumed or asserted.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetDensity (L : ℝ) (g : ℕ → ℝ) (B : Finset ℕ) : ℝ

Prime densities are already g(p) = ω(p)/p.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetDensity L g B = ∑ s ∈ B.powerset, MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.setWeight L s * ∏ p ∈ s, g p

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetDensity (L : ℝ) (g : ℕ → ℝ) (B : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetDensity L g B = ∑ s ∈ B.powerset, MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight L s * ∏ p ∈ s, g p

def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerBoundary (L : ℝ) (q : ℕ) (s : Finset ℕ) : Prop

The active odd tail whose next even cubic test fails.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerBoundary L q s = (↑(s.prod id) < L ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerAdmissibleSet L s ∧ ¬Even s.card ∧ L ≤ ↑(s.prod id) * ↑q ^ 3)

def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperBoundary (L : ℝ) (q : ℕ) (s : Finset ℕ) : Prop

The active even tail whose next odd cubic test fails.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperBoundary L q s = (↑(s.prod id) < L ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperAdmissibleSet L s ∧ Even s.card ∧ L ≤ ↑(s.prod id) * ↑q ^ 3)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoundaryDensity (L : ℝ) (g : ℕ → ℝ) (q : ℕ) (B : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoundaryDensity L g q B = ∑ s ∈ B.powerset, if MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.LowerBoundary L q s then ∏ p ∈ s, g p else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoundaryDensity (L : ℝ) (g : ℕ → ℝ) (q : ℕ) (B : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoundaryDensity L g q B = ∑ s ∈ B.powerset, if MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.UpperBoundary L q s then ∏ p ∈ s, g p else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetWeight_pair_eq_boundary {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hq : Nat.Prime q) (hqL : ↑q < L) (hqmin : ∀ p ∈ s, q ≤ p) : setWeight L s + setWeight L (insert q s) = -if LowerBoundary L q s then 1 else 0

Exact signed cancellation, including the failed even-prefix boundary.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight_pair_eq_boundary {L : ℝ} {q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hq : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) : upperSetWeight L s + upperSetWeight L (insert q s) = if UpperBoundary L q s then 1 else 0

Exact signed cancellation, including the failed odd-prefix boundary.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetDensity_insert_min (g : ℕ → ℝ) {L : ℝ} {q : ℕ} {B : Finset ℕ} (hqB : q ∉ B) (hq : Nat.Prime q) (hqL : ↑q < L) (hqmin : ∀ p ∈ B, q ≤ p) : lowerSetDensity L g (insert q B) = (1 - g q) * lowerSetDensity L g B - g q * lowerBoundaryDensity L g q B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetDensity_insert_min (g : ℕ → ℝ) {L : ℝ} {q : ℕ} {B : Finset ℕ} (hqB : q ∉ B) (hq : Nat.Prime q) (hqmin : ∀ p ∈ B, q ≤ p) : upperSetDensity L g (insert q B) = (1 - g q) * upperSetDensity L g B + g q * upperBoundaryDensity L g q B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_density_eq_setDensity {M : ℕ} (L : ℝ) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) (hM : Squarefree M) : ∑ d ∈ M.divisors, (lowerWeight M L) d * g d = lowerSetDensity L (⇑g) M.primeFactors

No complete multiplicativity is used: all divisors here are squarefree.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_density_eq_setDensity {M : ℕ} (L : ℝ) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) (hM : Squarefree M) : ∑ d ∈ M.divisors, (upperWeight M L) d * g d = upperSetDensity L (⇑g) M.primeFactors

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerDensityDefect (L : ℝ) (g : ℕ → ℝ) : List ℕ → ℝ

Explicit boundary accumulation in increasing-prime order. Earlier primes contribute their Euler factors; no error is defined by subtraction from the target density.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerDensityDefect L g [] = 0
• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerDensityDefect L g (q :: ps) = (1 - g q) * MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerDensityDefect L g ps + g q * MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoundaryDensity L g q ps.toFinset

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperDensityDefect (L : ℝ) (g : ℕ → ℝ) : List ℕ → ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperDensityDefect L g [] = 0
• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperDensityDefect L g (q :: ps) = (1 - g q) * MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperDensityDefect L g ps + g q * MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoundaryDensity L g q ps.toFinset

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetDensity_eq_euler_sub_defect (g : ℕ → ℝ) {L : ℝ} (hL : 1 < L) (ps : List ℕ) (hnd : ps.Nodup) (hsorted : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) ps) (hp : ∀ p ∈ ps, Nat.Prime p) (hcut : ∀ p ∈ ps, ↑p < L) : lowerSetDensity L g ps.toFinset = ∏ p ∈ ps.toFinset, (1 - g p) - lowerDensityDefect L g ps

The exact lower density is the Euler product minus its cubic boundaries.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetDensity_eq_euler_add_defect (g : ℕ → ℝ) {L : ℝ} (hL : 1 < L) (ps : List ℕ) (hnd : ps.Nodup) (hsorted : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) ps) (hp : ∀ p ∈ ps, Nat.Prime p) : upperSetDensity L g ps.toFinset = ∏ p ∈ ps.toFinset, (1 - g p) + upperDensityDefect L g ps

The exact upper density is the Euler product plus its cubic boundaries.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoundaryDensity_nonneg {L : ℝ} {g : ℕ → ℝ} {q : ℕ} {B : Finset ℕ} (hg : ∀ p ∈ B, 0 ≤ g p) : 0 ≤ lowerBoundaryDensity L g q B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoundaryDensity_nonneg {L : ℝ} {g : ℕ → ℝ} {q : ℕ} {B : Finset ℕ} (hg : ∀ p ∈ B, 0 ≤ g p) : 0 ≤ upperBoundaryDensity L g q B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerDensityDefect_nonneg {L : ℝ} {g : ℕ → ℝ} (ps : List ℕ) (hg : ∀ p ∈ ps, 0 ≤ g p ∧ g p ≤ 1) : 0 ≤ lowerDensityDefect L g ps

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperDensityDefect_nonneg {L : ℝ} {g : ℕ → ℝ} (ps : List ℕ) (hg : ∀ p ∈ ps, 0 ≤ g p ∧ g p ≤ 1) : 0 ≤ upperDensityDefect L g ps

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_density_eq_euler_sub_defect (B : Finset ℕ) {L : ℝ} (hL : 1 < L) (hB : ∀ p ∈ B, Nat.Prime p) (hcut : ∀ p ∈ B, ↑p < L) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : ∑ d ∈ (B.prod id).divisors, (lowerWeight (B.prod id) L) d * g d = ∏ p ∈ B, (1 - g p) - lowerDensityDefect L (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2)

Finite exact density formula for the existing real-level lower weight.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_density_eq_euler_add_defect (B : Finset ℕ) {L : ℝ} (hL : 1 < L) (hB : ∀ p ∈ B, Nat.Prime p) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : ∑ d ∈ (B.prod id).divisors, (upperWeight (B.prod id) L) d * g d = ∏ p ∈ B, (1 - g p) + upperDensityDefect L (⇑g) (B.sort fun (x1 x2 : ℕ) => x1 ≤ x2)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.primeDensity (ω : ArithmeticFunction ℝ) : ArithmeticFunction ℝ

The density convention in (22); division is pointwise, not convolution.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.primeDensity ω = { toFun := fun (n : ℕ) => ω n / ↑n, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.primeDensity_apply (ω : ArithmeticFunction ℝ) (n : ℕ) : (primeDensity ω) n = ω n / ↑n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.primeDensity_isMultiplicative {ω : ArithmeticFunction ℝ} (hω : ω.IsMultiplicative) : (primeDensity ω).IsMultiplicative

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallWeight_density_eq_euler_sub_defect (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : ∑ d ∈ ((geometricSmallPrimes P D ε).prod id).divisors, (lowerSmallWeight P D ε) d * g d = ∏ p ∈ geometricSmallPrimes P D ε, (1 - g p) - lowerDensityDefect (D ^ ε) (⇑g) ((geometricSmallPrimes P D ε).sort fun (x1 x2 : ℕ) => x1 ≤ x2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallWeight_density_eq_euler_add_defect (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) : ∑ d ∈ ((geometricSmallPrimes P D ε).prod id).divisors, (upperSmallWeight P D ε) d * g d = ∏ p ∈ geometricSmallPrimes P D ε, (1 - g p) + upperDensityDefect (D ^ ε) (⇑g) ((geometricSmallPrimes P D ε).sort fun (x1 x2 : ℕ) => x1 ≤ x2)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallWeight_density_bracket (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) {g : ArithmeticFunction ℝ} (hg : g.IsMultiplicative) (hg01 : ∀ p ∈ geometricSmallPrimes P D ε, 0 ≤ g p ∧ g p ≤ 1) : ∑ d ∈ ((geometricSmallPrimes P D ε).prod id).divisors, (lowerSmallWeight P D ε) d * g d ≤ ∏ p ∈ geometricSmallPrimes P D ε, (1 - g p) ∧ ∏ p ∈ geometricSmallPrimes P D ε, (1 - g p) ≤ ∑ d ∈ ((geometricSmallPrimes P D ε).prod id).divisors, (upperSmallWeight P D ε) d * g d

Both actual weights bracket the Euler product, with explicit nonnegative defects. This is not a bound for their size.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.smallWeight_source_density_identities (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) {ω : ArithmeticFunction ℝ} (hω : ω.IsMultiplicative) : ∑ d ∈ ((geometricSmallPrimes P D ε).prod id).divisors, (lowerSmallWeight P D ε) d * (ω d / ↑d) = ∏ p ∈ geometricSmallPrimes P D ε, (1 - ω p / ↑p) - lowerDensityDefect (D ^ ε) (⇑(primeDensity ω)) ((geometricSmallPrimes P D ε).sort fun (x1 x2 : ℕ) => x1 ≤ x2) ∧ ∑ d ∈ ((geometricSmallPrimes P D ε).prod id).divisors, (upperSmallWeight P D ε) d * (ω d / ↑d) = ∏ p ∈ geometricSmallPrimes P D ε, (1 - ω p / ↑p) + upperDensityDefect (D ^ ε) (⇑(primeDensity ω)) ((geometricSmallPrimes P D ε).sort fun (x1 x2 : ℕ) => x1 ≤ x2)

The exact finite identity in the source's ω(d)/d convention, with the original small weights on the left, not surrogate coefficients.