Documentation Verification Report

Defs

📁 Source: PrimeNumberTheoremAnd/Defs.lean

Statistics

Metric	Count
Definitions `Eθ`, `classicalBound`, `numericalBound`, `Eπ`, `bound`, `classicalBound`, `numericalBound`, `vinogradovBound`, `Eψ`, `bound`, `classicalBound`, `numericalBound`, `HasPrimeInInterval`, `log_thm`, `Li`, `M`, `Psi`, `admissible_bound`, `first_gap`, `first_gap_record`, `li`, `nth_prime`, `nth_prime_gap`, `pi`, `prime_gap_record`	25
Theorems `to_numericalBound`, `to_numericalBound`, `to_numericalBound`, `mono`	4
Total	29

Eθ

Definitions

Name	Category	Theorems
`classicalBound` 📖	MathDef	4 math math: `FKS2.remark_15`, `FKS2.proposition_13`, `PT.corollary_1`, `FKS2.corollary_14`
`numericalBound` 📖	MathDef	1 math math: `classicalBound.to_numericalBound`

Eθ.classicalBound

Theorems

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

Eπ

Definitions

Name	Category	Theorems
`bound` 📖	MathDef	1 math math: `FKS2.corollary_26`
`classicalBound` 📖	MathDef	5 math math: `FKS2.corollary_23`, `FKS2.theorem_3`, `JY.corollary_1_3`, `PT.corollary_2`, `FKS2.corollary_22`
`numericalBound` 📖	MathDef	1 math math: `classicalBound.to_numericalBound`
`vinogradovBound` 📖	MathDef	1 math math: `JY.theorem_1_4`

Eπ.classicalBound

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_numericalBound` 📖	mathematical	`Eπ.classicalBound`	`Eπ.numericalBound` `admissible_bound`	—	`admissible_bound.mono`

Eψ

Definitions

Name	Category	Theorems
`bound` 📖	MathDef	—
`classicalBound` 📖	MathDef	4 math math: `PT.theorem_1`, `FKS.FKS_corollary_1_3`, `FKS.theorem_1_2b`, `FKS.FKS_corollary_1_4`
`numericalBound` 📖	MathDef	2 math math: `classicalBound.to_numericalBound`, `PT.theorem_1`

Eψ.classicalBound

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_numericalBound` 📖	mathematical	`Eψ.classicalBound`	`Eψ.numericalBound` `admissible_bound`	—	`admissible_bound.mono`

HasPrimeInInterval

Definitions

Name	Category	Theorems
`log_thm` 📖	MathDef	2 math math: `Dusart.proposition_5_4`, `Dusart.proposition_5_4a`

(root)

Definitions

Name	Category	Theorems
`Eθ` 📖	CompOp	11 math math: `BKLNW.lem_6`, `Ramanujan.pi_bound_1`, `Dusart.theorem_4_2`, `Ramanujan.pi_bound_5`, `FKS2.theorem_6_1`, `Ramanujan.pi_bound_3`, `Ramanujan.pi_bound_4`, `BKLNW.cor_14_1`, `FKS2.lemma_12`, `Ramanujan.pi_bound_2`, `Ramanujan.pi_bound`
`Eπ` 📖	CompOp	6 math math: `FKS2.theorem_6`, `FKS2.corollary_24`, `FKS2.corollary_21`, `FKS2.theorem_6_1`, `FKS2.corollary_8`, `FKS2.theorem_6_alt`
`Eψ` 📖	CompOp	13 math math: `BKLNW_app.thm_14`, `FKS.lemma_5_3`, `FKS.theorem_1_1b`, `BKLNW_app.bklnw_thm_16`, `BKLNW_app.bklnw_eq_A_26`, `FKS.proposition_3_4`, `FKS.theorem_3_1`, `FKS.theorem_1_1`, `Dusart.proposition_3_2`, `BKLNW_app.bklnw_cor_15_1'`, `FKS.lemma_5_4`, `Buthe.theorem_2a`, `Dusart.theorem_3_3`
`HasPrimeInInterval` 📖	MathDef	23 math math: `Dusart.proposition_5_4c`, `CullyHugill2021.has_prime_in_interval`, `RamareSaouter2003.has_prime_in_interval`, `HasPrimeInInterval.iff_theta_ge`, `GourdonDemichel2004.has_prime_in_interval`, `Dudek2014.has_prime_in_interval`, `CarneiroEtAl2019RH.has_prime_in_interval`, `Dusart.corollary_5_5`, `Eθ.numericalBound.hasPrimeInInterval`, `PrimeGaps2014.has_prime_in_interval`, `PrimeGaps2024.has_prime_in_interval`, `Trudgian2016.has_prime_in_interval`, `HasPrimeInInterval.iff_pi_ge`, `RHPrimeInterval2002.has_prime_in_interval`, `Schoenfeld1976.has_prime_in_interval`, `Eθ.classicalBound.hasPrimeInInterval`, `theta_pos_implies_prime_in_interval`, `Eθ.hasPrimeInInterval`, `Dudek2015RH.has_prime_in_interval`, `prime_gap_record.hasPrimeInInterval`, `RamareSaouter2003.has_prime_in_interval_2`, `Dusart.proposition_5_4b`, `KadiriLumley.has_prime_in_interval`
`Li` 📖	CompOp	7 math math: `li.sub_Li`, `FKS2.hasDerivAt_Li`, `FKS2.theorem_6_3`, `FKS2.theorem_6_1`, `FKS2.lemma_20_a`, `FKS2.lemma_20_b`, `FKS2.lemma_19`
`M` 📖	CompOp	3 math math: `M_isLittleO`, `M_isLittleO'`, `M_log_identity`
`Psi` 📖	CompOp	2 math math: `M_log_identity`, `sum_mu_Lambda`
`admissible_bound` 📖	CompOp	7 math math: `Eψ.classicalBound.to_numericalBound`, `Eθ.classicalBound.to_numericalBound`, `FKS2.corollary_21`, `Eπ.classicalBound.to_numericalBound`, `BKLNW.cor_14_1`, `FKS2.corollary_14_small_adm`, `admissible_bound.mono`
`first_gap` 📖	CompOp	9 math math: `eSHP.first_gap_4`, `eSHP.first_gap_2`, `eSHP.first_gap_1`, `eSHP.first_gap_5`, `eSHP.first_gap_odd_gt_1`, `eSHP.first_gap_3`, `eSHP.first_gap_6`, `eSHP.first_gap_7`, `eSHP.exists_prime_gap`
`first_gap_record` 📖	MathDef	2 math math: `eSHP.table_9_prime_gap`, `eSHP.table_9_prime_gap_test`
`li` 📖	CompOp	9 math math: `Ramanujan.pi_error_identity`, `li.sub_Li`, `li.two_approx`, `li.two_approx_weak`, `Buthe.theorem_2d`, `li_eq_Li2Bounds_li`, `Buthe.theorem_2f`, `li2_symmetric_eq_li2`, `Buthe.theorem_2e`
`nth_prime` 📖	CompOp	7 math math: `eSHP.exists_prime_gap_record_le`, `nth_prime_asymp`, `log_nth_prime_asymp`, `eSHP.nth_prime_vals`, `pi_nth_prime_asymp`, `pi_nth_prime`, `tendsto_nth_prime_atTop`
`nth_prime_gap` 📖	CompOp	2 math math: `eSHP.exists_prime_gap_record_le`, `eSHP.max_prime_gap`
`pi` 📖	CompOp	20 math math: `Ramanujan.pi_error_identity`, `Dusart.corollary_5_3_a`, `Dusart.corollary_5_3_b`, `Ramanujan.pi_upper`, `Ramanujan.pi_lower`, `Dusart.theorem_5_1`, `Ramanujan.pi_upper_specific`, `Dusart.corollary_5_2_d`, `Ramanujan.pi_lower_specific`, `Dusart.corollary_5_2_b`, `Buthe.theorem_2f`, `Dusart.corollary_5_3_d`, `HasPrimeInInterval.iff_pi_ge`, `Dusart.corollary_5_2_f`, `Dusart.corollary_5_2_e`, `Dusart.corollary_5_2_c`, `Dusart.corollary_5_3_c`, `Buthe.theorem_2e`, `Dusart.corollary_5_2_a`, `Ramanujan.ramanujan_final`
`prime_gap_record` 📖	MathDef	3 math math: `eSHP.exists_prime_gap_record_le`, `eSHP.table_8_prime_gap_test`, `eSHP.table_8_prime_gap`

admissible_bound

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	—	`admissible_bound`	—	—

---

← Back to Index