eSHP

📁 Source: PrimeNumberTheoremAnd/eSHP.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_prime_gap`, `exists_prime_gap_record_le`, `first_gap_1`, `first_gap_2`, `first_gap_3`, `first_gap_4`, `first_gap_5`, `first_gap_6`, `first_gap_7`, `first_gap_odd_gt_1`, `max_prime_gap`, `nth_prime_vals`, `table_8_prime_gap`, `table_8_prime_gap_complete`, `table_8_prime_gap_complete_test`, `table_8_prime_gap_test`, `table_9_prime_gap`, `table_9_prime_gap_complete`, `table_9_prime_gap_complete_test`, `table_9_prime_gap_test`	20
Total	20
⚠️ With sorry `exists_prime_gap`, `table_8_prime_gap`, `table_8_prime_gap_complete`, `table_9_prime_gap`, `table_9_prime_gap_complete`	5

eSHP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_prime_gap` 📖 ⚠️	mathematical	—	`first_gap`	—	—
`exists_prime_gap_record_le` 📖	mathematical	—	`nth_prime` `nth_prime_gap` `prime_gap_record`	—	—
`first_gap_1` 📖	mathematical	—	`first_gap`	—	`nth_prime_vals`
`first_gap_2` 📖	mathematical	—	`first_gap`	—	`nth_prime_vals`
`first_gap_3` 📖	mathematical	—	`first_gap`	—	`first_gap_odd_gt_1`
`first_gap_4` 📖	mathematical	—	`first_gap`	—	—
`first_gap_5` 📖	mathematical	—	`first_gap`	—	`first_gap_odd_gt_1`
`first_gap_6` 📖	mathematical	—	`first_gap`	—	`nth_prime_vals`
`first_gap_7` 📖	mathematical	—	`first_gap`	—	`first_gap_odd_gt_1`
`first_gap_odd_gt_1` 📖	mathematical	—	`first_gap`	—	—
`max_prime_gap` 📖	mathematical	`nth_prime`	`nth_prime_gap`	—	`exists_prime_gap_record_le` `table_8_prime_gap_complete`
`nth_prime_vals` 📖	mathematical	—	`nth_prime`	—	—
`table_8_prime_gap` 📖 ⚠️	mathematical	`table_8`	`prime_gap_record`	—	—
`table_8_prime_gap_complete` 📖 ⚠️	mathematical	`prime_gap_record`	`table_8`	—	—
`table_8_prime_gap_complete_test` 📖	mathematical	`prime_gap_record`	`table_8`	—	—
`table_8_prime_gap_test` 📖	mathematical	`table_8`	`prime_gap_record`	—	—
`table_9_prime_gap` 📖 ⚠️	mathematical	`table_9`	`first_gap_record`	—	—
`table_9_prime_gap_complete` 📖 ⚠️	mathematical	`first_gap_record`	`table_9`	—	—
`table_9_prime_gap_complete_test` 📖	mathematical	`first_gap_record`	`table_9`	—	`first_gap_7` `first_gap_6` `first_gap_5` `first_gap_4` `first_gap_3` `first_gap_2` `first_gap_1`
`table_9_prime_gap_test` 📖	mathematical	`table_9`	`first_gap_record`	—	—

---

← Back to Index