Dusart

📁 Source: PrimeNumberTheoremAnd/Dusart.lean

Statistics

Metric	Count
Definitions `Table1`, `Table2`, `Table_3_3`, `Table_4_2`	4
Theorems `corollary_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
Total	40
⚠️ With sorry `corollary_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`, `lemma_4_1`, `lemma_5_10a`, `lemma_5_10b`, `lemma_5_14`, `massias_robin_thm_Bv`, `proposition_3_2`, `proposition_4_4`, `proposition_5_11a`, `proposition_5_11b`, `proposition_5_12`, `proposition_5_15`, `proposition_5_16`, `proposition_5_4c`, `theorem_3_3`, `theorem_4_2`, `theorem_5_1`, `theorem_5_6`, `theorem_5_7`, `theorem_5_9a`	30

Dusart

Definitions

Name	Category	Theorems
`Table1` 📖	CompOp	—
`Table2` 📖	CompOp	—
`Table_3_3` 📖	CompOp	—
`Table_4_2` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends 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`	—	`proposition_5_4`
`lemma_4_1` 📖 ⚠️	—	`Table2`	—	—	—
`lemma_5_10a` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`lemma_5_10b` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`lemma_5_14` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`massias_robin_thm_Bv` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`proposition_3_2` 📖 ⚠️	mathematical	`Table1`	`Eψ`	—	—
`proposition_4_3` 📖	—	—	—	—	—
`proposition_4_4` 📖 ⚠️	—	—	—	—	—
`proposition_5_11a` 📖 ⚠️	mathematical	`nth_prime'`	`nth_prime'`	—	—
`proposition_5_11b` 📖 ⚠️	mathematical	`nth_prime'`	`nth_prime'`	—	—
`proposition_5_12` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`proposition_5_15` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`proposition_5_16` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`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`	—	`prime_gap_record.hasPrimeInInterval` `eSHP.table_8_prime_gap` `eSHP.max_prime_gap`
`proposition_5_4c` 📖 ⚠️	mathematical	—	`HasPrimeInInterval`	—	—
`theorem_3_3` 📖 ⚠️	mathematical	`Table_3_3`	`Eψ`	—	—
`theorem_4_2` 📖 ⚠️	mathematical	`Table_4_2`	`Eθ`	—	—
`theorem_5_1` 📖 ⚠️	mathematical	—	`pi`	—	—
`theorem_5_6` 📖 ⚠️	mathematical	—	`meisselMertensConstant`	—	—
`theorem_5_7` 📖 ⚠️	mathematical	—	`mertensConstant`	—	—
`theorem_5_9a` 📖 ⚠️	—	—	—	—	—
`theorem_5_9b` 📖	—	—	—	—	`theorem_5_9a`

---

← Back to Index