Documentation Verification Report

SecondarySummary

📁 Source: PrimeNumberTheoremAnd/SecondarySummary.lean

Statistics

Metric	Count
Definitions `Table_1`, `eps_0`	2
Theorems `corollary_1_3`, `theorem_1_4`, `admissible_bound_weaken`, `corollary_1`, `corollary_2`, `table_1_bounds`, `theorem_1`, `has_prime_in_interval`, `lemma_1`, `theorem_1_psi`, `theorem_1_theta`, `theorem_2`	12
Total	14
⚠️ With sorry `theorem_1_4`, `theorem_1`, `has_prime_in_interval`, `lemma_1`, `theorem_1_psi`, `theorem_1_theta`, `theorem_2`	7

JY

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`corollary_1_3` 📖	mathematical	—	`Eπ.classicalBound`	—	`FKS2.corollary_22`
`theorem_1_4` 📖 ⚠️	mathematical	—	`Eπ.vinogradovBound`	—	—

PT

Definitions

Name	Category	Theorems
`Table_1` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`admissible_bound_weaken` 📖	mathematical	—	`admissible_bound`	—	—
`corollary_1` 📖	mathematical	`Table_1`	`Eθ.classicalBound`	—	`table_1_bounds` `FKS2.corollary_14` `admissible_bound_weaken`
`corollary_2` 📖	mathematical	—	`Eπ.classicalBound`	—	`FKS2.corollary_22`
`table_1_bounds` 📖	—	`Table_1`	—	—	—
`theorem_1` 📖 ⚠️	mathematical	`Table_1`	`Eψ.classicalBound` `Eψ.numericalBound`	—	—

Trudgian2016

Definitions

Name	Category	Theorems
`eps_0` 📖	CompOp	2 math math: `theorem_1_psi`, `theorem_1_theta`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`has_prime_in_interval` 📖 ⚠️	mathematical	—	`HasPrimeInInterval`	—	—
`lemma_1` 📖 ⚠️	mathematical	—	`Eθ.numericalBound`	—	—
`theorem_1_psi` 📖 ⚠️	mathematical	—	`Eψ.numericalBound` `eps_0`	—	—
`theorem_1_theta` 📖 ⚠️	mathematical	—	`Eθ.numericalBound` `eps_0`	—	—
`theorem_2` 📖 ⚠️	mathematical	—	`Eπ.numericalBound`	—	—

---

← Back to Index