Documentation Verification Report

SelbergSieve

📁 Source: Mathlib/NumberTheory/SelbergSieve.lean

Statistics

Metric	Count
Definitions `BoundingSieve`, `IsUpperMoebius`, `errSum`, `mainSum`, `multSum`, `nu`, `prodPrimes`, `rem`, `siftedSum`, `support`, `totalMass`, `weights`, `evalBoundingSieveWeights`, `SelbergSieve`, `level`, `toBoundingSieve`	16
Theorems `multSum_eq_main_err`, `nu_lt_one_of_dvd_prodPrimes`, `nu_lt_one_of_prime`, `nu_mult`, `nu_ne_zero`, `nu_pos_of_dvd_prodPrimes`, `nu_pos_of_prime`, `one_le_y`, `prodPrimes_ne_zero`, `prodPrimes_squarefree`, `prod_primeFactors_nu`, `siftedSum_eq_sum_support_mul_ite`, `siftedSum_le_mainSum_errSum_of_upperMoebius`, `siftedSum_le_sum_of_upperMoebius`, `squarefree_of_dvd_prodPrimes`, `squarefree_of_mem_divisors_prodPrimes`, `weights_nonneg`, `one_le_level`	18
Total	34

BoundingSieve

Definitions

Name	Category	Theorems
`IsUpperMoebius` 📖	MathDef	—
`errSum` 📖	CompOp	1 math math: `siftedSum_le_mainSum_errSum_of_upperMoebius`
`mainSum` 📖	CompOp	1 math math: `siftedSum_le_mainSum_errSum_of_upperMoebius`
`multSum` 📖	CompOp	2 math math: `siftedSum_le_sum_of_upperMoebius`, `multSum_eq_main_err`
`nu` 📖	CompOp	7 math math: `nu_lt_one_of_dvd_prodPrimes`, `nu_lt_one_of_prime`, `nu_pos_of_dvd_prodPrimes`, `nu_mult`, `nu_pos_of_prime`, `multSum_eq_main_err`, `prod_primeFactors_nu`
`prodPrimes` 📖	CompOp	3 math math: `prodPrimes_squarefree`, `siftedSum_eq_sum_support_mul_ite`, `siftedSum_le_sum_of_upperMoebius`
`rem` 📖	CompOp	1 math math: `multSum_eq_main_err`
`siftedSum` 📖	CompOp	3 math math: `siftedSum_eq_sum_support_mul_ite`, `siftedSum_le_sum_of_upperMoebius`, `siftedSum_le_mainSum_errSum_of_upperMoebius`
`support` 📖	CompOp	1 math math: `siftedSum_eq_sum_support_mul_ite`
`totalMass` 📖	CompOp	2 math math: `siftedSum_le_mainSum_errSum_of_upperMoebius`, `multSum_eq_main_err`
`weights` 📖	CompOp	2 math math: `siftedSum_eq_sum_support_mul_ite`, `weights_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multSum_eq_main_err` 📖	mathematical	—	`multSum` `Real` `Real.instAdd` `Real.instMul` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `nu` `totalMass` `rem`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`nu_lt_one_of_dvd_prodPrimes` 📖	mathematical	`prodPrimes`	`Real` `Real.instLT` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `nu` `Real.instOne`	—	`Squarefree.squarefree_of_dvd` `prodPrimes_squarefree` `Squarefree.ne_zero` `Nat.instNontrivial` `prod_primeFactors_nu` `Finset.prod_lt_prod_of_nonempty` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instNontrivial` `nu_pos_of_prime` `Dvd.dvd.trans` `nu_lt_one_of_prime` `Nat.mem_primeFactors_of_ne_zero` `Finset.prod_const_one`
`nu_lt_one_of_prime` 📖	mathematical	`Nat.Prime` `prodPrimes`	`Real` `Real.instLT` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `nu` `Real.instOne`	—	—
`nu_mult` 📖	mathematical	—	`ArithmeticFunction.IsMultiplicative` `Real` `Real.instMonoidWithZero` `nu`	—	—
`nu_ne_zero` 📖	—	`prodPrimes`	—	—	`ne_of_gt` `nu_pos_of_dvd_prodPrimes`
`nu_pos_of_dvd_prodPrimes` 📖	mathematical	`prodPrimes`	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `ArithmeticFunction` `ArithmeticFunction.instFunLikeNat` `nu`	—	`Finset.prod_pos` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instNontrivial` `Nat.prime_of_mem_primeFactors` `Dvd.dvd.trans` `Nat.dvd_of_mem_primeFactors` `nu_pos_of_prime` `prod_primeFactors_nu`
`nu_pos_of_prime` 📖	mathematical	`Nat.Prime` `prodPrimes`	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `ArithmeticFunction` `ArithmeticFunction.instFunLikeNat` `nu`	—	—
`one_le_y` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `SelbergSieve.level`	—	`SelbergSieve.one_le_level`
`prodPrimes_ne_zero` 📖	—	—	—	—	`Squarefree.ne_zero` `Nat.instNontrivial` `prodPrimes_squarefree`
`prodPrimes_squarefree` 📖	mathematical	—	`Squarefree` `Nat.instMonoid` `prodPrimes`	—	—
`prod_primeFactors_nu` 📖	mathematical	`prodPrimes`	`Finset.prod` `Real` `Real.instCommMonoid` `Nat.primeFactors` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `nu`	—	`ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors` `nu_mult` `subset_rfl` `Finset.instReflSubset` `Nat.prod_primeFactors_of_squarefree` `Squarefree.squarefree_of_dvd` `prodPrimes_squarefree`
`siftedSum_eq_sum_support_mul_ite` 📖	mathematical	—	`siftedSum` `Finset.sum` `Real` `Real.instAddCommMonoid` `support` `Real.instMul` `weights` `prodPrimes` `Real.instOne` `Real.instZero`	—	`Finset.sum_congr` `mul_ite` `mul_one` `MulZeroClass.mul_zero`
`siftedSum_le_mainSum_errSum_of_upperMoebius` 📖	mathematical	`IsUpperMoebius`	`Real` `Real.instLE` `siftedSum` `Real.instAdd` `Real.instMul` `totalMass` `mainSum` `errSum`	—	`siftedSum_le_sum_of_upperMoebius` `mainSum.eq_1` `Finset.mul_sum` `Finset.sum_add_distrib` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `errSum.eq_1` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.sum_le_sum` `abs_mul` `Real.instIsOrderedRing` `le_abs_self`
`siftedSum_le_sum_of_upperMoebius` 📖	mathematical	`IsUpperMoebius`	`Real` `Real.instLE` `siftedSum` `Finset.sum` `Real.instAddCommMonoid` `Nat.divisors` `prodPrimes` `Real.instMul` `multSum`	—	`siftedSum_eq_sum_support_mul_ite` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `weights_nonneg` `Finset.sum_congr` `Finset.mul_sum` `Nat.divisors_filter_dvd_of_dvd` `prodPrimes_ne_zero` `Finset.ext` `Finset.filter.congr_simp` `Finset.sum_comm` `mul_comm`
`squarefree_of_dvd_prodPrimes` 📖	mathematical	`prodPrimes`	`Squarefree` `Nat.instMonoid`	—	`Squarefree.squarefree_of_dvd` `prodPrimes_squarefree`
`squarefree_of_mem_divisors_prodPrimes` 📖	mathematical	`Finset` `Finset.instMembership` `Nat.divisors` `prodPrimes`	`Squarefree` `Nat.instMonoid`	—	`Squarefree.squarefree_of_dvd` `prodPrimes_squarefree`
`weights_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `weights`	—	—

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalBoundingSieveWeights` 📖	CompOp	—

SelbergSieve

Definitions

Name	Category	Theorems
`level` 📖	CompOp	2 math math: `BoundingSieve.one_le_y`, `one_le_level`
`toBoundingSieve` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_le_level` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `level`	—	—

(root)

Definitions

Name	Category	Theorems
`BoundingSieve` 📖	CompData	—
`SelbergSieve` 📖	CompData	—

---

← Back to Index