Generic Selberg main-term identities

Identities for the Selberg terms of an arbitrary BoundingSieve: the prime value of g, and the closed factorization of the divisor sum Σ_{d | P} g(d) = ∏_{p | P} (1 - ν(p))⁻¹ over the squarefree sifting product. These are the finite algebraic core of the Selberg main term, shared by every Goldbach-type sieve problem.

theorem AnalyticNumberTheory.Sieve.selbergTerm_prime {S : BoundingSieve} {p : ℕ} (hp : Nat.Prime p) : BoundingSieve.selbergTerms p = S.nu p * (1 - S.nu p)⁻¹

The Selberg term of any BoundingSieve at a prime is ν(p) · (1 - ν(p))⁻¹.

theorem AnalyticNumberTheory.Sieve.selbergSum_eq_prod_inv {S : BoundingSieve} : ∑ d ∈ S.prodPrimes.divisors, BoundingSieve.selbergTerms d = ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p)⁻¹

The Selberg divisor sum of any BoundingSieve factors over its prime factors: Σ_{d | P} g(d) = ∏_{p | P} (1 - ν(p))⁻¹.