theorem
MathlibNt.SieveTheory.LiLiuPrereqWF.boundedOne_fouvryTau
{f : ArithmeticFunction ℝ}
(hf : BoundedOne f)
(n : ℕ)
:
The order-one bound includes the zero coefficient.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuPrereqWF.boundedOne_fouvryTau · compiled type and proof/definition references.
theorem
MathlibNt.SieveTheory.LiLiuPrereqWF.wellFactorable_to_signed
{f : ArithmeticFunction ℝ}
{Q : ℝ}
(hf : WellFactorable f Q)
:
AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable 1 Q fun (n : ℕ) => f n
No squarefree mask, coefficient rescaling, or change of real level.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuPrereqWF.wellFactorable_to_signed · compiled type and proof/definition references.
theorem
MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm_signedWellFactorable
(upper : Bool)
(P : Finset ℕ)
{Q η : ℝ}
(z : ℝ)
(t : List ℕ)
(hQ : 0 ≤ Q)
(hD : 2 ≤ externalInternalLevel Q η)
(hη : 0 < η)
(hηsmall : η < 1 / 8)
(ht : t ∈ externalTags upper P (externalInternalLevel Q η) η z)
:
AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable 1 Q fun (n : ℕ) =>
(externalTerm upper P (externalInternalLevel Q η) η z t) n
Actual normalized external family members at the original external level.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm_signedWellFactorable · compiled type and proof/definition references.