Documentation Verification Report

Dusart

šŸ“ Source: PrimeNumberTheoremAnd/Dusart.lean

Statistics

MetricCount
DefinitionsTable1, Table2, Table_3_3, Table_4_2
4
Theoremscorollary_4_5, corollary_5_2_a, corollary_5_2_b, corollary_5_2_c, corollary_5_2_d, corollary_5_2_e, corollary_5_2_f, corollary_5_3_a, corollary_5_3_b, corollary_5_3_c, corollary_5_3_d, corollary_5_5, lemma_4_1, lemma_5_10a, lemma_5_10b, lemma_5_14, massias_robin_thm_Bv, proposition_3_2, proposition_4_3, proposition_4_4, proposition_5_11a, proposition_5_11b, proposition_5_12, proposition_5_15, proposition_5_16, proposition_5_4, proposition_5_4a, proposition_5_4b, proposition_5_4c, theorem_3_3, theorem_4_2, theorem_5_1, theorem_5_6, theorem_5_7, theorem_5_9a, theorem_5_9b
36
Total40
āš ļø With sorrycorollary_4_5, corollary_5_2_a, corollary_5_2_b, corollary_5_2_c, corollary_5_2_d, corollary_5_2_e, corollary_5_2_f, corollary_5_3_a, corollary_5_3_b, corollary_5_3_c, corollary_5_3_d, corollary_5_5, lemma_4_1, lemma_5_10a, lemma_5_10b, lemma_5_14, massias_robin_thm_Bv, proposition_3_2, proposition_4_3, proposition_4_4, proposition_5_11a, proposition_5_11b, proposition_5_12, proposition_5_15, proposition_5_16, proposition_5_4b, proposition_5_4c, theorem_3_3, theorem_4_2, theorem_5_1, theorem_5_6, theorem_5_7, theorem_5_9a, theorem_5_9b
34

Dusart

Definitions

NameCategoryTheorems
Table1 šŸ“–CompOpā€”
Table2 šŸ“–CompOpā€”
Table_3_3 šŸ“–CompOpā€”
Table_4_2 šŸ“–CompOpā€”

Theorems

NameKindAssumesProvesValidatesDepends On
corollary_4_5 šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
corollary_5_2_a šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_2_b šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_2_c šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_2_d šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_2_e šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_2_f šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_3_a šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_3_b šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_3_c šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_3_d šŸ“– āš ļømathematicalā€”piā€”ā€”
corollary_5_5 šŸ“– āš ļømathematicalā€”HasPrimeInIntervalā€”ā€”
lemma_4_1 šŸ“– āš ļøā€”Table2ā€”ā€”ā€”
lemma_5_10a šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
lemma_5_10b šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
lemma_5_14 šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
massias_robin_thm_Bv šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_3_2 šŸ“– āš ļømathematicalTable1EĻˆā€”ā€”
proposition_4_3 šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_4_4 šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_5_11a šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_5_11b šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_5_12 šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_5_15 šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_5_16 šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
proposition_5_4 šŸ“–mathematicalā€”HasPrimeInInterval.log_thmā€”proposition_5_4c
proposition_5_4a
proposition_5_4b
proposition_5_4a šŸ“–mathematicalā€”HasPrimeInInterval.log_thmā€”theorem_4_2
EĪø.hasPrimeInInterval
proposition_5_4b šŸ“– āš ļømathematicalā€”HasPrimeInIntervalā€”ā€”
proposition_5_4c šŸ“– āš ļømathematicalā€”HasPrimeInIntervalā€”ā€”
theorem_3_3 šŸ“– āš ļømathematicalTable_3_3EĻˆā€”ā€”
theorem_4_2 šŸ“– āš ļømathematicalTable_4_2EĪøā€”ā€”
theorem_5_1 šŸ“– āš ļømathematicalā€”piā€”ā€”
theorem_5_6 šŸ“– āš ļømathematicalā€”meisselMertensConstantā€”ā€”
theorem_5_7 šŸ“– āš ļømathematicalā€”mertensConstantā€”ā€”
theorem_5_9a šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”
theorem_5_9b šŸ“– āš ļøā€”ā€”ā€”ā€”ā€”

---

ā† Back to Index