Documentation Verification Report

Chebyshev

📁 Source: PrimeNumberTheoremAnd/Chebyshev.lean

Statistics

Metric	Count
Definitions `E`, `T`, `U`, `a`, `ν`	5
Theorems `E_nu_bound`, `E_nu_eq_one`, `E_nu_period`, `eq_sum_Lambda`, `ge`, `le`, `weighted_eq_sum`, `U_bound`, `a_bound`, `a_simpl`, `nu_sum_div_eq_zero`, `psi_diff_le_weighted`, `psi_diff_upper`, `psi_ge_weighted`, `psi_lower`, `psi_num`, `psi_num_2`, `psi_upper`, `psi_upper_clean`	19
Total	24
⚠️ With sorry `U_bound`, `psi_num_2`, `psi_upper_clean`	3

Chebyshev

Definitions

Name	Category	Theorems
`E` 📖	CompOp	4 math math: `E_nu_period`, `T.weighted_eq_sum`, `E_nu_bound`, `E_nu_eq_one`
`T` 📖	CompOp	4 math math: `T.ge`, `T.le`, `T.eq_sum_Lambda`, `T.weighted_eq_sum`
`U` 📖	CompOp	3 math math: `psi_ge_weighted`, `U_bound`, `psi_diff_le_weighted`
`a` 📖	CompOp	6 math math: `psi_diff_upper`, `a_bound`, `U_bound`, `psi_upper`, `psi_lower`, `a_simpl`
`ν` 📖	CompOp	4 math math: `E_nu_period`, `nu_sum_div_eq_zero`, `E_nu_bound`, `E_nu_eq_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`E_nu_bound` 📖	mathematical	—	`E` `ν`	—	`E.eq_1` `ν.eq_1` `E_nu_period`
`E_nu_eq_one` 📖	mathematical	—	`E` `ν`	—	`E.eq_1` `ν.eq_1`
`E_nu_period` 📖	mathematical	—	`E` `ν`	—	`E.eq_1` `ν.eq_1`
`U_bound` 📖 ⚠️	mathematical	—	`U` `a`	—	—
`a_bound` 📖	mathematical	—	`a`	—	`a_simpl` `LogTables.log_2_gt` `LogTables.log_2_lt` `LogTables.log_3_gt` `LogTables.log_5_gt` `LogTables.log_3_lt` `LogTables.log_5_lt`
`a_simpl` 📖	mathematical	—	`a`	—	—
`nu_sum_div_eq_zero` 📖	mathematical	—	`ν`	—	—
`psi_diff_le_weighted` 📖	mathematical	—	`U`	—	`T.weighted_eq_sum` `Finset.Ioc_eq_Icc` `E_nu_eq_one` `E_nu_bound`
`psi_diff_upper` 📖	mathematical	—	`a`	—	`psi_diff_le_weighted` `U_bound`
`psi_ge_weighted` 📖	mathematical	—	`U`	—	`T.weighted_eq_sum` `Finset.Ioc_eq_Icc` `E_nu_bound`
`psi_lower` 📖	mathematical	—	`a`	—	`psi_ge_weighted` `U_bound`
`psi_num` 📖	—	—	—	—	`LogTables.log_7_lt` `LogTables.log_11_lt` `LogTables.log_13_lt` `LogTables.log_17_lt` `LogTables.log_19_lt` `LogTables.log_2_lt` `LogTables.log_3_lt` `LogTables.log_5_lt`
`psi_num_2` 📖 ⚠️	—	—	—	—	—
`psi_upper` 📖	mathematical	—	`a`	—	`psi_diff_upper` `psi_num` `a_bound`
`psi_upper_clean` 📖 ⚠️	—	—	—	—	—

Chebyshev.T

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_sum_Lambda` 📖	mathematical	—	`Chebyshev.T`	—	`Finset.Ioc_eq_Icc`
`ge` 📖	mathematical	—	`Chebyshev.T`	—	—
`le` 📖	mathematical	—	`Chebyshev.T`	—	`eq_1`
`weighted_eq_sum` 📖	mathematical	—	`Chebyshev.T` `Chebyshev.E`	—	`eq_sum_Lambda`

---

← Back to Index