Documentation Verification Report

SelbergBounds

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

Statistics

Metric	Count
Definitions `CompletelyMultiplicative`	1
Theorems `apply_pow`, `id`, `isMultiplicative`, `pdiv`, `pmul`, `zeta`, `squarefree_dvd_pow`, `boundingSum_ge_log`, `boundingSum_ge_sum`, `prime_dvd_primorial_iff`, `primorial_squarefree`, `prodDistinctPrimes_squarefree`, `prod_factors_one_div_compMult_ge`, `prod_factors_sum_pow_compMult`, `prod_primes_dvd_of_dvd`, `rem_sum_le_of_const`, `selbergBoundingSum_ge_sum_div`, `siftedSum_eq`, `sqrt_le_self`, `zeta_lt_self_of_prime`, `zeta_pos_of_prime`	21
Total	22

Sieve

Definitions

Name	Category	Theorems
`CompletelyMultiplicative` 📖	MathDef	2 math math: `CompletelyMultiplicative.id`, `CompletelyMultiplicative.zeta`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundingSum_ge_log` 📖	mathematical	—	`SelbergSieve.selbergBoundingSum`	—	`boundingSum_ge_sum` `Aux.log_le_sum_inv`
`boundingSum_ge_sum` 📖	mathematical	—	`SelbergSieve.selbergBoundingSum`	—	`selbergBoundingSum_ge_sum_div` `CompletelyMultiplicative.pdiv` `CompletelyMultiplicative.zeta` `CompletelyMultiplicative.id`
`prime_dvd_primorial_iff` 📖	—	—	—	—	—
`primorial_squarefree` 📖	—	—	—	—	`prodDistinctPrimes_squarefree`
`prodDistinctPrimes_squarefree` 📖	—	—	—	—	—
`prod_factors_one_div_compMult_ge` 📖	—	`CompletelyMultiplicative`	—	—	`CompletelyMultiplicative.isMultiplicative` `CompletelyMultiplicative.apply_pow`
`prod_factors_sum_pow_compMult` 📖	—	`CompletelyMultiplicative`	—	—	`CompletelyMultiplicative.isMultiplicative`
`prod_primes_dvd_of_dvd` 📖	—	—	—	—	—
`rem_sum_le_of_const` 📖	—	—	—	—	`Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow`
`selbergBoundingSum_ge_sum_div` 📖	mathematical	`CompletelyMultiplicative`	`SelbergSieve.selbergBoundingSum`	—	`prod_factors_sum_pow_compMult` `SelbergSieve.selbergTerms_apply` `prod_factors_one_div_compMult_ge` `Nat.squarefree_dvd_pow` `prod_primes_dvd_of_dvd` `sqrt_le_self`
`siftedSum_eq` 📖	—	—	—	—	`prime_dvd_primorial_iff`
`sqrt_le_self` 📖	—	—	—	—	—
`zeta_lt_self_of_prime` 📖	—	—	—	—	—
`zeta_pos_of_prime` 📖	—	—	—	—	—

Sieve.CompletelyMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_pow` 📖	—	`Sieve.CompletelyMultiplicative`	—	—	—
`id` 📖	mathematical	—	`Sieve.CompletelyMultiplicative`	—	—
`isMultiplicative` 📖	—	`Sieve.CompletelyMultiplicative`	—	—	—
`pdiv` 📖	—	`Sieve.CompletelyMultiplicative`	—	—	—
`pmul` 📖	—	`Sieve.CompletelyMultiplicative`	—	—	—
`zeta` 📖	mathematical	—	`Sieve.CompletelyMultiplicative`	—	—

Sieve.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree_dvd_pow` 📖	—	—	—	—	—

---

← Back to Index