Documentation Verification Report

Chebyshev

📁 Source: PrimeNumberTheoremAnd/Chebyshev.lean

Statistics

Metric	Count
Definitions `E`, `T`, `U`, `a`, `e`, `ν`	6
Theorems `E_nu_bound`, `E_nu_eq_one`, `E_nu_period`, `abs_sum_le`, `eq_sum_Lambda`, `ge`, `le`, `weighted_eq_sum`, `U_bound`, `lemma_1`, `lemma_2`, `lemma_3`, `lemma_4`, `lemma_5`, `lemma_6`, `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`	26
Total	32

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	5 math math: `T.ge`, `T.le`, `T.eq_sum_Lambda`, `T.weighted_eq_sum`, `U_bound.lemma_1`
`U` 📖	CompOp	4 math math: `psi_ge_weighted`, `U_bound.lemma_3`, `U_bound`, `psi_diff_le_weighted`
`a` 📖	CompOp	7 math math: `psi_diff_upper`, `U_bound.lemma_4`, `a_bound`, `U_bound`, `psi_upper`, `psi_lower`, `a_simpl`
`e` 📖	CompOp	3 math math: `U_bound.lemma_3`, `U_bound.lemma_2`, `U_bound.lemma_1`
`ν` 📖	CompOp	8 math math: `E_nu_period`, `U_bound.lemma_4`, `U_bound.lemma_3`, `U_bound.lemma_5`, `nu_sum_div_eq_zero`, `U_bound.lemma_6`, `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`	—	`U_bound.lemma_3` `U_bound.lemma_4` `U_bound.lemma_5` `U_bound.lemma_6` `Finsupp.abs_sum_le` `U_bound.lemma_2` `LogTables.log_2_gt` `LogTables.log_3_gt` `LogTables.log_5_gt` `LogTables.log_30_gt`
`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`	—	`U_bound` `psi_diff_le_weighted`
`psi_ge_weighted` 📖	mathematical	—	`U`	—	`T.weighted_eq_sum` `Finset.Ioc_eq_Icc` `E_nu_bound`
`psi_lower` 📖	mathematical	—	`a`	—	`U_bound` `psi_ge_weighted`
`psi_num` 📖	—	—	—	—	`LogTables.log_2_lt` `LogTables.log_3_lt` `LogTables.log_5_lt` `LogTables.log_7_lt` `LogTables.log_11_lt` `LogTables.log_13_lt` `LogTables.log_17_lt` `LogTables.log_19_lt` `LogTables.log_23_lt` `LogTables.log_29_lt`
`psi_num_2` 📖	—	—	—	—	—
`psi_upper` 📖	mathematical	—	`a`	—	`psi_diff_upper` `psi_num` `a_bound`
`psi_upper_clean` 📖	—	—	—	—	`psi_num_2` `psi_diff_upper` `a_bound`

Chebyshev.Finsupp

Theorems

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

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`

Chebyshev.U_bound

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lemma_1` 📖	mathematical	—	`Chebyshev.T` `Chebyshev.e`	—	—
`lemma_2` 📖	mathematical	—	`Chebyshev.e`	—	`Chebyshev.T.ge` `Chebyshev.T.le`
`lemma_3` 📖	mathematical	—	`Chebyshev.U` `Chebyshev.ν` `Chebyshev.e`	—	`lemma_1`
`lemma_4` 📖	mathematical	—	`Chebyshev.ν` `Chebyshev.a`	—	`Chebyshev.ν.eq_1` `Chebyshev.a.eq_1`
`lemma_5` 📖	mathematical	—	`Chebyshev.ν`	—	`Chebyshev.ν.eq_1`
`lemma_6` 📖	mathematical	—	`Chebyshev.ν`	—	`Chebyshev.ν.eq_1`

---

← Back to Index