PrimeInInterval

📁 Source: PrimeNumberTheoremAnd/PrimeInInterval.lean

Statistics

Metric	Count
Definitions	0
Theorems hasPrimeInInterval, hasPrimeInInterval, hasPrimeInInterval, iff_pi_ge, iff_theta_ge, hasPrimeInInterval, theta_pos_implies_prime_in_interval	7
Total	7

Eθ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPrimeInInterval 📖	mathematical	Eθ	HasPrimeInInterval	—	HasPrimeInInterval.iff_theta_ge

Eθ.classicalBound

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPrimeInInterval 📖	mathematical	Eθ.classicalBound admissible_bound	HasPrimeInInterval	—	to_numericalBound Eθ.numericalBound.hasPrimeInInterval

Eθ.numericalBound

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPrimeInInterval 📖	mathematical	Eθ.numericalBound	HasPrimeInInterval	—	Eθ.hasPrimeInInterval

HasPrimeInInterval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_pi_ge 📖	mathematical	—	HasPrimeInInterval pi	—	prime_in_gap'
iff_theta_ge 📖	mathematical	—	HasPrimeInInterval	—	theta_pos_implies_prime_in_interval

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
theta_pos_implies_prime_in_interval 📖	mathematical	—	HasPrimeInInterval	—	—

prime_gap_record

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPrimeInInterval 📖	mathematical	prime_gap_record	HasPrimeInInterval	—	—

---

← Back to Index