SecondarySummary

📁 Source: PrimeNumberTheoremAnd/SecondarySummary.lean

Statistics

Metric	Count
Definitions Table_2, Table_1	2
Theorems has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, corollary_1_3, theorem_1_4, has_prime_in_interval, corollary_1, corollary_2, theorem_1, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval_2, has_prime_in_interval, has_prime_in_interval	18
Total	20
⚠️ With sorry has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, theorem_1_4, has_prime_in_interval, corollary_1, theorem_1, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval, has_prime_in_interval_2, has_prime_in_interval, has_prime_in_interval	16

CarneiroEtAl2019RH

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

CullyHugill2021

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

Dudek2014

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

Dudek2015RH

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

GourdonDemichel2004

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

JY

Theorems

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

KadiriLumley

Definitions

Name	Category	Theorems
Table_2 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	Table_2	HasPrimeInInterval	—	—

PT

Definitions

Name	Category	Theorems
Table_1 📖	CompOp	—

Theorems

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

PrimeGaps2014

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

PrimeGaps2024

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

RHPrimeInterval2002

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

RamareSaouter2003

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—
has_prime_in_interval_2 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

Schoenfeld1976

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

Trudgian2016

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_prime_in_interval 📖 ⚠️	mathematical	—	HasPrimeInInterval	—	—

---

← Back to Index