Finite sieve direction for one normalized signed box convention

The positive/negative choices are those of Iwaniec (17)--(18): the favourable sign uses weakly decreasing boxes at the original level; the opposite sign uses distinct boxes and the upper endpoints. Each squarefree prime set contributes once. This is the divided-power convention, NOT the raw labelled-slot sum or its factorial-copy expansion.

The two endpoint functions enclose each prime. The exact geometric specialization and identification with the common full-integer box weights are separate from the pointwise sieve inequalities proved here.

def MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSupport (upper : Bool) (b : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : Prop

Rounded strict support and all source cubic tests.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSupport upper b D s = (∏ p ∈ s, b p < D ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSetAdmissible upper b D s)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSupport_mono {upper : Bool} {b c : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hb : ∀ p ∈ s, 0 ≤ b p) (hbc : ∀ p ∈ s, b p ≤ c p) (h : RoundedSupport upper c D s) : RoundedSupport upper b D s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSupport_cast_lower_iff (D : ℝ) (s : Finset ℕ) : RoundedSupport false (fun (p : ℕ) => ↑p) D s ↔ ↑(s.prod id) < D ∧ SmallRosser.LowerAdmissibleSet D s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSupport_cast_upper_iff (D : ℝ) (s : Finset ℕ) : RoundedSupport true (fun (p : ℕ) => ↑p) D s ↔ ↑(s.prod id) < D ∧ SmallRosser.UpperAdmissibleSet D s

def MathlibNt.SieveTheory.LiLiuPrereqWF.TightRoundedSupport (upper : Bool) (b c : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : Prop

The source's strictly decreasing-box side, before the sign is applied.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.TightRoundedSupport upper b c D s = (Set.InjOn b ↑s ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSupport upper c D s)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedUpperSet (b c : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedUpperSet b c D s = if Even s.card then if MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSupport true b D s then 1 else 0 else if MathlibNt.SieveTheory.LiLiuPrereqWF.TightRoundedSupport true b c D s then -1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerSet (b c : ℕ → ℝ) (D : ℝ) (s : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerSet b c D s = if Even s.card then if MathlibNt.SieveTheory.LiLiuPrereqWF.TightRoundedSupport false b c D s then 1 else 0 else if MathlibNt.SieveTheory.LiLiuPrereqWF.RoundedSupport false b D s then -1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.upperSetWeight_le_normalizedUpperSet {b c : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hb : ∀ p ∈ s, 0 ≤ b p) (hbp : ∀ p ∈ s, b p ≤ ↑p) (hpc : ∀ p ∈ s, ↑p ≤ c p) : SmallRosser.upperSetWeight D s ≤ normalizedUpperSet b c D s

Removing negative terms or adding positive terms only raises the upper Rosser coefficient. Repeated-box prime sets are still counted exactly once.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerSet_le_setWeight {b c : ℕ → ℝ} {D : ℝ} {s : Finset ℕ} (hb : ∀ p ∈ s, 0 ≤ b p) (hbp : ∀ p ∈ s, b p ≤ ↑p) (hpc : ∀ p ∈ s, ↑p ≤ c p) : normalizedLowerSet b c D s ≤ SmallRosser.setWeight D s

The lower sign reverses BOTH choices: odd terms are enlarged, while positive even terms with a repeated box are omitted.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedUpperWeight (M : ℕ) (D : ℝ) (b c : ℕ → ℝ) : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedUpperWeight M D b c = { toFun := fun (n : ℕ) => if n ∈ M.divisors then MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedUpperSet b c D n.primeFactors else 0, map_zero' := ⋯ }

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerWeight (M : ℕ) (D : ℝ) (b c : ℕ → ℝ) : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerWeight M D b c = { toFun := fun (n : ℕ) => if n ∈ M.divisors then MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerSet b c D n.primeFactors else 0, map_zero' := ⋯ }

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.upperWeight_le_normalizedUpperWeight {M : ℕ} {D : ℝ} {b c : ℕ → ℝ} (hM : Squarefree M) (hb : ∀ p ∈ M.primeFactors, 0 ≤ b p) (hbp : ∀ p ∈ M.primeFactors, b p ≤ ↑p) (hpc : ∀ p ∈ M.primeFactors, ↑p ≤ c p) (n : ℕ) : (SmallRosser.upperWeight M D) n ≤ (normalizedUpperWeight M D b c) n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerWeight_le_lowerWeight {M : ℕ} {D : ℝ} {b c : ℕ → ℝ} (hM : Squarefree M) (hb : ∀ p ∈ M.primeFactors, 0 ≤ b p) (hbp : ∀ p ∈ M.primeFactors, b p ≤ ↑p) (hpc : ∀ p ∈ M.primeFactors, ↑p ≤ c p) (n : ℕ) : (normalizedLowerWeight M D b c) n ≤ (SmallRosser.lowerWeight M D) n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedUpperWeight_divisor_sum {M n : ℕ} {D : ℝ} {b c : ℕ → ℝ} (hM : Squarefree M) (hD : 1 < D) (hn : n ≠ 0) (hb : ∀ p ∈ M.primeFactors, 0 ≤ b p) (hbp : ∀ p ∈ M.primeFactors, b p ≤ ↑p) (hpc : ∀ p ∈ M.primeFactors, ↑p ≤ c p) : (if n.Coprime M then 1 else 0) ≤ ∑ d ∈ n.divisors, (normalizedUpperWeight M D b c) d

Genuine finite upper-sieve direction, not an assumption on the new aggregate. It holds at every positive integer, including prime powers.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.normalizedLowerWeight_divisor_sum {M n : ℕ} {D : ℝ} {b c : ℕ → ℝ} (hM : Squarefree M) (hD : ∀ p ∈ M.primeFactors, ↑p < D) (hb : ∀ p ∈ M.primeFactors, 0 ≤ b p) (hbp : ∀ p ∈ M.primeFactors, b p ≤ ↑p) (hpc : ∀ p ∈ M.primeFactors, ↑p ≤ c p) : ∑ d ∈ n.divisors, (normalizedLowerWeight M D b c) d ≤ if n.Coprime M then 1 else 0

The omitted lower positive pieces and enlarged negative pieces retain the lower direction. The prime cutoff is the genuine lower Rosser hypothesis.