Documentation Verification Report

TMEEMT

📁 Source: PrimeNumberTheoremAnd/TMEEMT.lean

Statistics

Metric	Count
Definitions `pi_r`, `corollary_5_5_copy`, `proposition_5_4_copy`, `Table_2`, `lemma_3_2_bound`, `Table_1`	6
Theorems `sum_prime_lower`, `sum_prime_upper`, `has_prime_in_interval_1`, `has_prime_in_interval_2`, `theorem_a`, `theorem_b`, `theorem_2a`, `theorem_2b`, `theorem_2c`, `theorem_2d`, `prime_gap`, `has_prime_in_interval`, `p_n_asym`, `has_prime_in_interval`, `sum_log_prime`, `sum_loglog_prime`, `theorem_a`, `theorem_b`, `theorem_c`, `theorem_d`, `theorem_e`, `theorem_f`, `theorem_g`, `theorem_h`, `has_prime_in_interval`, `has_prime_in_interval`, `theta_improv_1`, `theta_improv_2`, `p_n_lower`, `p_n_upper`, `pi_inequality`, `theorem_a`, `theorem_b`, `theorem_c`, `theorem_d`, `psi_bound`, `psi_bound`, `has_prime_in_interval`, `psi_bound_1`, `psi_bound_2`, `psi_bound_3`, `has_prime_in_interval`, `p_n_lower`, `sum_p_inv_a`, `sum_p_inv_b`, `sum_p_inv_c`, `sum_p_inv_d`, `psi_bound`, `has_prime_in_interval`, `has_prime_in_interval`, `has_prime_in_interval`, `p_n_lower`, `p_n_upper`, `theorem_a`, `theorem_b`, `theorem_c`, `theorem_d`, `von_mangoldt_sum_1a`, `von_mangoldt_sum_1b`, `von_mangoldt_sum_1c`, `von_mangoldt_sum_1d`, `von_mangoldt_sum_2`, `lemma_3_2_a`, `lemma_3_2_b`, `lemma_3_2_c`, `has_prime_in_interval`, `has_prime_in_interval_2`, `p_n_lower`, `p_n_lower_const1`, `p_n_gt_1`, `p_n_gt_2`, `p_n_lt_2`, `p_n_lower`, `p_n_upper`, `has_prime_in_interval`, `sum_prime_bound`	76
Total	82
⚠️ With sorry `sum_prime_lower`, `sum_prime_upper`, `has_prime_in_interval_1`, `has_prime_in_interval_2`, `theorem_a`, `theorem_b`, `theorem_2a`, `theorem_2b`, `theorem_2c`, `theorem_2d`, `prime_gap`, `has_prime_in_interval`, `p_n_asym`, `has_prime_in_interval`, `sum_log_prime`, `sum_loglog_prime`, `theorem_a`, `theorem_b`, `theorem_c`, `theorem_d`, `theorem_e`, `theorem_f`, `theorem_g`, `theorem_h`, `has_prime_in_interval`, `has_prime_in_interval`, `p_n_lower`, `p_n_upper`, `theorem_b`, `theorem_c`, `has_prime_in_interval`, `psi_bound_1`, `psi_bound_3`, `has_prime_in_interval`, `p_n_lower`, `sum_p_inv_a`, `sum_p_inv_b`, `sum_p_inv_c`, `sum_p_inv_d`, `psi_bound`, `has_prime_in_interval`, `p_n_upper`, `theorem_b`, `theorem_c`, `theorem_d`, `von_mangoldt_sum_1a`, `von_mangoldt_sum_1b`, `von_mangoldt_sum_1c`, `von_mangoldt_sum_1d`, `von_mangoldt_sum_2`, `lemma_3_2_a`, `lemma_3_2_b`, `lemma_3_2_c`, `has_prime_in_interval`, `p_n_lower`, `p_n_lower_const1`, `p_n_lt_2`, `p_n_upper`, `has_prime_in_interval`, `sum_prime_bound`	60

Axler

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_prime_lower` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`sum_prime_upper` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—

Axler2018

Theorems

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

Buthe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`theorem_a` 📖 ⚠️	—	—	—	—	—
`theorem_b` 📖 ⚠️	mathematical	—	`li` `pi`	—	—

Buthe2

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`theorem_2a` 📖 ⚠️	—	—	—	—	—
`theorem_2b` 📖 ⚠️	—	—	—	—	—
`theorem_2c` 📖 ⚠️	mathematical	—	`pi_star` `li`	—	—
`theorem_2d` 📖 ⚠️	mathematical	—	`pi` `li`	—	—

CMS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prime_gap` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—

CarneiroEtAl2019RH

Theorems

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

Cipolla

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_n_asym` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—

CullyHugill2021

Theorems

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

DeKoninckLetendre

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_log_prime` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`sum_loglog_prime` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—

DelegliseNicolas

Definitions

Name	Category	Theorems
`pi_r` 📖	CompOp	8 math math: `theorem_f`, `theorem_b`, `theorem_a`, `theorem_c`, `theorem_g`, `theorem_h`, `theorem_d`, `theorem_e`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`theorem_a` 📖 ⚠️	mathematical	—	`pi_r`	—	—
`theorem_b` 📖 ⚠️	mathematical	—	`pi_r`	—	—
`theorem_c` 📖 ⚠️	mathematical	—	`pi_r`	—	—
`theorem_d` 📖 ⚠️	mathematical	—	`pi_r`	—	—
`theorem_e` 📖 ⚠️	mathematical	—	`pi_r`	—	—
`theorem_f` 📖 ⚠️	mathematical	—	`pi_r`	—	—
`theorem_g` 📖 ⚠️	mathematical	—	`pi_r`	—	—
`theorem_h` 📖 ⚠️	mathematical	—	`pi_r`	—	—

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`	—	—

Dusart

Definitions

Name	Category	Theorems
`corollary_5_5_copy` 📖	CompOp	—
`proposition_5_4_copy` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`theta_improv_1` 📖	—	—	—	—	`theorem_4_2`
`theta_improv_2` 📖	—	—	—	—	`theorem_4_2`

Dusart1999

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_n_lower` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`p_n_upper` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`pi_inequality` 📖	mathematical	—	`pi`	—	`Dusart.corollary_5_3_a`
`theorem_a` 📖	—	—	—	—	—
`theorem_b` 📖 ⚠️	—	—	—	—	—
`theorem_c` 📖 ⚠️	—	—	—	—	—
`theorem_d` 📖	—	—	—	—	`Dusart.theorem_4_2`

FKS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`psi_bound` 📖	—	—	—	—	`FKS_corollary_1_4`

FaberKadiri

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`psi_bound` 📖	—	—	—	—	`Dusart.theorem_3_3`

GourdonDemichel2004

Theorems

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

JY

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`psi_bound_1` 📖 ⚠️	—	—	—	—	—
`psi_bound_2` 📖	—	—	—	—	`FKS.FKS_corollary_1_4`
`psi_bound_3` 📖 ⚠️	—	—	—	—	—

KadiriLumley

Definitions

Name	Category	Theorems
`Table_2` 📖	CompOp	—

Theorems

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

MassiasRobin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_n_lower` 📖 ⚠️	mathematical	`nth_prime'`	`nth_prime'`	—	—

Mawia

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_p_inv_a` 📖 ⚠️	mathematical	—	`meisselMertensConstant`	—	—
`sum_p_inv_b` 📖 ⚠️	mathematical	—	`meisselMertensConstant`	—	—
`sum_p_inv_c` 📖 ⚠️	mathematical	—	`meisselMertensConstant`	—	—
`sum_p_inv_d` 📖 ⚠️	mathematical	—	`meisselMertensConstant`	—	—

PT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`psi_bound` 📖 ⚠️	—	—	—	—	—

PrimeGaps2014

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`has_prime_in_interval` 📖	mathematical	—	`HasPrimeInInterval`	—	`GourdonDemichel2004.has_prime_in_interval`

PrimeGaps2024

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`has_prime_in_interval` 📖	mathematical	—	`HasPrimeInInterval`	—	`JY.psi_bound_1` `Dusart.corollary_4_5` `theta_pos_implies_prime_in_interval`

RHPrimeInterval2002

Theorems

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

RS_prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_n_lower` 📖	mathematical	—	`nth_prime'`	—	`RS_prime_helper.p_n_lower_small` `RS_prime_helper.p_n_lower_large`
`p_n_upper` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`theorem_a` 📖	—	—	—	—	`theorem_12`
`theorem_b` 📖 ⚠️	mathematical	—	`pi`	—	—
`theorem_c` 📖 ⚠️	—	—	—	—	—
`theorem_d` 📖 ⚠️	—	—	—	—	—

Ramare2013

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`von_mangoldt_sum_1a` 📖 ⚠️	—	—	—	—	—
`von_mangoldt_sum_1b` 📖 ⚠️	—	—	—	—	—
`von_mangoldt_sum_1c` 📖 ⚠️	—	—	—	—	—
`von_mangoldt_sum_1d` 📖 ⚠️	—	—	—	—	—
`von_mangoldt_sum_2` 📖 ⚠️	—	—	—	—	—

Ramare2016

Definitions

Name	Category	Theorems
`lemma_3_2_bound` 📖	MathDef	3 math math: `lemma_3_2_a`, `lemma_3_2_c`, `lemma_3_2_b`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lemma_3_2_a` 📖 ⚠️	mathematical	—	`lemma_3_2_bound`	—	—
`lemma_3_2_b` 📖 ⚠️	mathematical	—	`lemma_3_2_bound`	—	—
`lemma_3_2_c` 📖 ⚠️	mathematical	—	`lemma_3_2_bound`	—	—

RamareSaouter2003

Theorems

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

Robin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_n_lower` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—
`p_n_lower_const1` 📖 ⚠️	mathematical	`nth_prime'`	`nth_prime'`	—	—

Rosser1938

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_n_gt_1` 📖	mathematical	—	`nth_prime'`	—	`RS_prime_helper.count_prime_le_imp_le_nth` `count_prime_127_le_30` `count_prime_113_le_29` `count_prime_109_le_28` `count_prime_107_le_27` `count_prime_103_le_26` `count_prime_101_le_25` `count_prime_97_le_24` `count_prime_89_le_23` `count_prime_83_le_22` `count_prime_79_le_21` `count_prime_73_le_20` `count_prime_71_le_19` `count_prime_67_le_18` `count_prime_61_le_17` `count_prime_59_le_16` `count_prime_53_le_15` `count_prime_47_le_14` `count_prime_43_le_13` `count_prime_41_le_12` `count_prime_37_le_11` `count_prime_31_le_10` `count_prime_29_le_9` `count_prime_23_le_8` `count_prime_19_le_7` `count_prime_17_le_6` `count_prime_13_le_5` `count_prime_11_le_4` `count_prime_7_le_3` `count_prime_5_le_2` `count_prime_3_le_1` `Dusart.corollary_5_3_b` `LogTables.exp_1_112_lt` `RS_prime_helper.pi_nth_prime'` `LogTables.log_32_gt` `LogTables.log_2_353_gt` `LogTables.log_3_2_gt`
`p_n_gt_2` 📖	mathematical	—	`nth_prime'`	—	`RS_prime_helper.p_n_lower_small` `RS_prime_helper.p_n_lower_large`
`p_n_lt_2` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—

Rosser1941

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_n_lower` 📖	mathematical	—	`nth_prime'`	—	`RS_prime_helper.p_n_lower_small` `RS_prime_helper.p_n_lower_large`
`p_n_upper` 📖 ⚠️	mathematical	—	`nth_prime'`	—	—

Schoenfeld1976

Theorems

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

Trevino

Definitions

Name	Category	Theorems
`Table_1` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_prime_bound` 📖 ⚠️	—	`Table_1`	—	—	—

---

← Back to Index