theorem
AnalyticNumberTheory.LargeSieve.weightedPrimitiveFamilyMass_le_triangular
(Q : ℕ)
(S : Finset ℕ)
(hS : S ⊆ Finset.Icc 1 Q)
:
A primitive family supported on conductors in [1,Q] has weighted mass at
most the triangular number Q(Q+1)/2.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.weightedPrimitiveFamilyMass_le_triangular · compiled type and proof/definition references.
The full conductor interval version of weightedPrimitiveFamilyMass_le_triangular.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.weightedPrimitiveFamilyMass_Icc_le_triangular · compiled type and proof/definition references.