Natural producer formulas for the actual real-level coefficients

These equalities expose exactly the natural-number prefix tests and the parity sign used by LinearSieve.lean in the frozen source. They prove the formulas for the existing local functions; they do not introduce a second weight or assume equality to it.

This module itself needs no producer import. The checked named-producer identification is in LiLiuPrereqWFProducerBridge.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerAdmissibleSet_iff_natCeil (L : ℝ) (s : Finset ℕ) : LowerAdmissibleSet L s ↔ ∀ p ∈ s, Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperAdmissibleSet_iff_natCeil (L : ℝ) (s : Finset ℕ) : UpperAdmissibleSet L s ↔ ∀ p ∈ s, ¬Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerWeight_eq_natCeil_tests (M n : ℕ) (L : ℝ) : (lowerWeight M L) n = if n ∈ M.divisors ∧ n < ⌈L⌉₊ ∧ ∀ p ∈ n.primeFactors, Even {q ∈ n.primeFactors | p ≤ q}.card → {q ∈ n.primeFactors | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊ then if Even n.primeFactors.card then 1 else -1 else 0

The entire lower coefficient, including its support and parity sign.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperWeight_eq_natCeil_tests (M n : ℕ) (L : ℝ) : (upperWeight M L) n = if n ∈ M.divisors ∧ n < ⌈L⌉₊ ∧ ∀ p ∈ n.primeFactors, ¬Even {q ∈ n.primeFactors | p ≤ q}.card → {q ∈ n.primeFactors | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊ then if Even n.primeFactors.card then 1 else -1 else 0

The upper condition is the odd-position test, not the lower even test.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.setWeight_eq_natCeil_tests (L : ℝ) (s : Finset ℕ) : setWeight L s = if s.prod id < ⌈L⌉₊ ∧ ∀ p ∈ s, Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊ then if Even s.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetWeight_eq_natCeil_tests (L : ℝ) (s : Finset ℕ) : upperSetWeight L s = if s.prod id < ⌈L⌉₊ ∧ ∀ p ∈ s, ¬Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊ then if Even s.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSetDensity_eq_natCeil_tests (L : ℝ) (g : ℕ → ℝ) (B : Finset ℕ) : lowerSetDensity L g B = ∑ s ∈ B.powerset, (if s.prod id < ⌈L⌉₊ ∧ ∀ p ∈ s, Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊ then if Even s.card then 1 else -1 else 0) * ∏ p ∈ s, g p

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSetDensity_eq_natCeil_tests (L : ℝ) (g : ℕ → ℝ) (B : Finset ℕ) : upperSetDensity L g B = ∑ s ∈ B.powerset, (if s.prod id < ⌈L⌉₊ ∧ ∀ p ∈ s, ¬Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < ⌈L⌉₊ then if Even s.card then 1 else -1 else 0) * ∏ p ∈ s, g p