theorem
MathlibNt.SieveTheory.suzukiElementaryMass_le_pow_div_factorial
(S : BoundingSieve)
(n z : ℕ)
:
suzukiElementaryMass S n z ≤ (∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p) ^ n / ↑n.factorial
The elementary symmetric mass is bounded by the corresponding power sum, with the exact factorial denominator.
Inspect dependencies
MathlibNt.SieveTheory.suzukiElementaryMass_le_pow_div_factorial · compiled type and proof/definition references.
theorem
MathlibNt.SieveTheory.suzukiSourceV_le_pow_div_factorial
(S : BoundingSieve)
(n D z : ℕ)
:
suzukiSourceV S n D z ≤ (∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p) ^ n / ↑n.factorial
Lemma 14.1 factorial bound, combining source domination by the elementary symmetric mass with its ordered-tuple/factorial estimate.
Inspect dependencies
MathlibNt.SieveTheory.suzukiSourceV_le_pow_div_factorial · compiled type and proof/definition references.