Documentation Verification Report

Selberg

📁 Source: PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean

Statistics

Metric	Count
Definitions `selbergBoundingSum`, `selbergMuPlus`, `selbergUbSieve`, `selbergWeights`	4
Theorems `eq_gcd_mul_of_dvd_of_coprime`, `mainSum_eq_diag_quad_form`, `selbergBoundingSum_ge`, `selbergBoundingSum_ne_zero`, `selbergBoundingSum_nonneg`, `selbergBoundingSum_pos`, `selbergWeights_diagonalisation`, `selbergWeights_eq_dvds_sum`, `selbergWeights_eq_zero`, `selbergWeights_eq_zero_of_not_dvd`, `selbergWeights_mul_mu_nonneg`, `selberg_bound_muPlus`, `selberg_bound_simple`, `selberg_bound_simple_errSum`, `selberg_bound_simple_mainSum`, `selberg_bound_weights`, `selbergμPlus_eq_zero`, `sum_mul_subst`, `weight_one_of_selberg`	19
Total	23

SelbergSieve

Definitions

Name	Category	Theorems
`selbergBoundingSum` 📖	CompOp	11 math math: `selbergBoundingSum_pos`, `selbergBoundingSum_nonneg`, `Sieve.boundingSum_ge_log`, `selberg_bound_simple_mainSum`, `selbergWeights_eq_dvds_sum`, `BrunTitchmarsh.boudingSum_ge`, `Sieve.selbergBoundingSum_ge_sum_div`, `selbergBoundingSum_ge`, `Sieve.boundingSum_ge_sum`, `selberg_bound_simple`, `selbergWeights_diagonalisation`
`selbergMuPlus` 📖	CompOp	5 math math: `selberg_bound_muPlus`, `selberg_bound_simple_mainSum`, `mainSum_eq_diag_quad_form`, `selbergμPlus_eq_zero`, `selberg_bound_simple_errSum`
`selbergUbSieve` 📖	CompOp	—
`selbergWeights` 📖	CompOp	9 math math: `selbergWeights_mul_mu_nonneg`, `selbergWeights_eq_zero_of_not_dvd`, `selbergWeights_eq_dvds_sum`, `selberg_bound_weights`, `selbergWeights_eq_zero`, `mainSum_eq_diag_quad_form`, `selbergBoundingSum_ge`, `weight_one_of_selberg`, `selbergWeights_diagonalisation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_gcd_mul_of_dvd_of_coprime` 📖	—	—	—	—	—
`mainSum_eq_diag_quad_form` 📖	mathematical	—	`selbergMuPlus` `selbergTerms` `selbergWeights`	—	`lambdaSquared_mainSum_eq_diag_quad_form`
`selbergBoundingSum_ge` 📖	mathematical	—	`selbergBoundingSum` `selbergWeights`	—	`sum_mul_subst` `selbergTerms_mult` `selbergTerms_pos` `conv_selbergTerms_eq_selbergTerms_mul_nu` `selbergBoundingSum_pos`
`selbergBoundingSum_ne_zero` 📖	—	—	—	—	`selbergBoundingSum_pos`
`selbergBoundingSum_nonneg` 📖	mathematical	—	`selbergBoundingSum`	—	`selbergBoundingSum_pos`
`selbergBoundingSum_pos` 📖	mathematical	—	`selbergBoundingSum`	—	`selbergTerms_pos`
`selbergWeights_diagonalisation` 📖	mathematical	—	`selbergWeights` `selbergTerms` `selbergBoundingSum`	—	`selbergWeights_eq_dvds_sum` `Aux.moebius_inv_dvd_lower_bound_real`
`selbergWeights_eq_dvds_sum` 📖	mathematical	—	`selbergWeights` `selbergBoundingSum` `selbergTerms`	—	`sum_mul_subst` `selbergTerms_mult`
`selbergWeights_eq_zero` 📖	mathematical	—	`selbergWeights`	—	—
`selbergWeights_eq_zero_of_not_dvd` 📖	mathematical	—	`selbergWeights`	—	`selbergWeights.eq_1`
`selbergWeights_mul_mu_nonneg` 📖	mathematical	—	`selbergWeights`	—	`selbergTerms_pos` `selbergBoundingSum_nonneg`
`selberg_bound_muPlus` 📖	mathematical	—	`selbergMuPlus`	—	`selberg_bound_weights`
`selberg_bound_simple` 📖	mathematical	—	`selbergBoundingSum`	—	`siftedSum_le_mainSum_errSum_of_UpperBoundSieve` `selberg_bound_simple_mainSum` `selberg_bound_simple_errSum`
`selberg_bound_simple_errSum` 📖	mathematical	—	`selbergMuPlus`	—	`selberg_bound_muPlus` `selbergμPlus_eq_zero`
`selberg_bound_simple_mainSum` 📖	mathematical	—	`selbergMuPlus` `selbergBoundingSum`	—	`mainSum_eq_diag_quad_form` `selbergWeights_diagonalisation` `selbergTerms_pos` `selbergBoundingSum_pos`
`selberg_bound_weights` 📖	mathematical	—	`selbergWeights`	—	`selbergBoundingSum_ge` `selbergBoundingSum_pos` `selbergWeights_mul_mu_nonneg` `selbergWeights_eq_zero_of_not_dvd`
`selbergμPlus_eq_zero` 📖	mathematical	—	`selbergMuPlus`	—	`lambdaSquared_eq_zero_of_support` `selbergWeights_eq_zero`
`sum_mul_subst` 📖	—	—	—	—	—
`weight_one_of_selberg` 📖	mathematical	—	`selbergWeights`	—	`selbergTerms_mult` `selbergBoundingSum_ne_zero`

---

← Back to Index