theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryMass_nonneg (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) (hnu : ∀ p ∈ P, 0 ≤ nu p) : 0 ≤ lowerRosserBoundaryMass nu D q P

Every finite cubic-boundary mass is nonnegative when the local density is.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryAccum_nonneg (nu : ℕ → ℝ) (D : ℕ) (P : Finset ℕ) (qs : List ℕ) (hnu : ∀ p ∈ List.foldr insert P qs, 0 ≤ nu p) (hnuOne : ∀ p ∈ List.foldr insert P qs, nu p ≤ 1) : 0 ≤ lowerRosserBoundaryAccum nu D P qs

The fully iterated lower-Rosser boundary loss has a fixed nonnegative sign. This is the useful replacement for taking the absolute value of an opaque source-to-density discrepancy.