Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsLowerMoebius`, `LowerBoundSieve`, `μMinus`, `UpperBoundSieve`, `μPlus`, `delta`, `lambdaSquared`, `lbToμMinus`, `selbergTerms`, `ubToμPlus`	10
Theorems `hμMinus`, `hμPlus`, `conv_selbergTerms_eq_selbergTerms_mul_nu`, `lambdaSquared_eq_zero_of_support`, `lambdaSquared_mainSum_eq_diag_quad_form`, `lambdaSquared_mainSum_eq_quad_form`, `nu_eq_conv_one_div_selbergTerms`, `nu_lt_self_of_dvd_prodPrimes`, `nu_ne_zero_of_mem_divisors_prodPrimes`, `one_div_selbergTerms_eq_conv_moebius_nu`, `selbergTerms_apply`, `selbergTerms_mult`, `selbergTerms_pos`, `siftedSum_as_delta`, `siftedSum_le_mainSum_errSum_of_UpperBoundSieve`, `upperMoebius_of_lambda_sq`, `upper_bound_of_UpperBoundSieve`	17
Total	27

SelbergSieve

Definitions

Name	Category	Theorems
`IsLowerMoebius` 📖	MathDef	1 math math: `LowerBoundSieve.hμMinus`
`LowerBoundSieve` 📖	CompData	—
`UpperBoundSieve` 📖	CompData	—
`delta` 📖	CompOp	1 math math: `siftedSum_as_delta`
`lambdaSquared` 📖	CompOp	4 math math: `lambdaSquared_eq_zero_of_support`, `lambdaSquared_mainSum_eq_diag_quad_form`, `upperMoebius_of_lambda_sq`, `lambdaSquared_mainSum_eq_quad_form`
`lbToμMinus` 📖	CompOp	—
`selbergTerms` 📖	CompOp	10 math math: `selbergTerms_mult`, `selbergTerms_pos`, `selbergWeights_eq_dvds_sum`, `mainSum_eq_diag_quad_form`, `one_div_selbergTerms_eq_conv_moebius_nu`, `selbergTerms_apply`, `lambdaSquared_mainSum_eq_diag_quad_form`, `selbergWeights_diagonalisation`, `conv_selbergTerms_eq_selbergTerms_mul_nu`, `nu_eq_conv_one_div_selbergTerms`
`ubToμPlus` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conv_selbergTerms_eq_selbergTerms_mul_nu` 📖	mathematical	—	`selbergTerms`	—	`Aux.sum_over_dvd_ite` `Aux.div_mult_of_dvd_squarefree` `selbergTerms_mult` `selbergTerms_pos` `nu_eq_conv_one_div_selbergTerms`
`lambdaSquared_eq_zero_of_support` 📖	mathematical	—	`lambdaSquared`	—	—
`lambdaSquared_mainSum_eq_diag_quad_form` 📖	mathematical	—	`lambdaSquared` `selbergTerms`	—	`lambdaSquared_mainSum_eq_quad_form` `nu_eq_conv_one_div_selbergTerms`
`lambdaSquared_mainSum_eq_quad_form` 📖	mathematical	—	`lambdaSquared`	—	`Aux.conv_lambda_sq_larger_sum`
`nu_eq_conv_one_div_selbergTerms` 📖	mathematical	—	`selbergTerms`	—	`one_div_selbergTerms_eq_conv_moebius_nu`
`nu_lt_self_of_dvd_prodPrimes` 📖	—	—	—	—	—
`nu_ne_zero_of_mem_divisors_prodPrimes` 📖	—	—	—	—	—
`one_div_selbergTerms_eq_conv_moebius_nu` 📖	mathematical	—	`selbergTerms`	—	`selbergTerms_apply` `Aux.div_mult_of_dvd_squarefree` `Aux.multiplicative_zero_of_zero_dvd`
`selbergTerms_apply` 📖	mathematical	—	`selbergTerms`	—	—
`selbergTerms_mult` 📖	mathematical	—	`selbergTerms`	—	—
`selbergTerms_pos` 📖	mathematical	—	`selbergTerms`	—	`selbergTerms_apply`
`siftedSum_as_delta` 📖	mathematical	—	`delta`	—	—
`siftedSum_le_mainSum_errSum_of_UpperBoundSieve` 📖	mathematical	—	`UpperBoundSieve.μPlus`	—	`UpperBoundSieve.hμPlus`
`upperMoebius_of_lambda_sq` 📖	mathematical	—	`lambdaSquared`	—	`Aux.conv_lambda_sq_larger_sum`
`upper_bound_of_UpperBoundSieve` 📖	mathematical	—	`UpperBoundSieve.μPlus`	—	`UpperBoundSieve.hμPlus`

SelbergSieve.LowerBoundSieve

Definitions

Name	Category	Theorems
`μMinus` 📖	CompOp	1 math math: `hμMinus`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hμMinus` 📖	mathematical	—	`SelbergSieve.IsLowerMoebius` `μMinus`	—	—

SelbergSieve.UpperBoundSieve

Definitions

Name	Category	Theorems
`μPlus` 📖	CompOp	3 math math: `SelbergSieve.upper_bound_of_UpperBoundSieve`, `SelbergSieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve`, `hμPlus`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hμPlus` 📖	mathematical	—	`μPlus`	—	—

---

← Back to Index