theorem AnalyticNumberTheory.LargeSieve.weightedPrimitiveFamilyMass_le_triangular (Q : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) : weightedPrimitiveFamilyMass S ≤ ↑Q * (↑Q + 1) / 2

A primitive family supported on conductors in [1,Q] has weighted mass at most the triangular number Q(Q+1)/2.

theorem AnalyticNumberTheory.LargeSieve.weightedPrimitiveFamilyMass_Icc_le_triangular (Q : ℕ) : weightedPrimitiveFamilyMass (Finset.Icc 1 Q) ≤ ↑Q * (↑Q + 1) / 2

The full conductor interval version of weightedPrimitiveFamilyMass_le_triangular.