Documentation Verification Report

BKLNW_tables

📁 Source: PrimeNumberTheoremAnd/BKLNW_tables.lean

Statistics

Metric	Count
Definitions `check_row_prop`, `exp_neg_one_ub`, `table_14`, `table_14_margin`	4
Theorems `check_row_prop_of_bounds`, `exp_neg_le_pow`, `exp_neg_le_pow'`, `exp_neg_le_rpow`, `exp_neg_le_rpow'`, `rpow_le_of_pow_le`, `table_14_check`	7
Total	11

BKLNW

Definitions

Name	Category	Theorems
`check_row_prop` 📖	MathDef	2 math math: `check_row_prop_of_bounds`, `table_14_check`
`exp_neg_one_ub` 📖	CompOp	4 math math: `exp_neg_le_rpow`, `exp_neg_le_pow`, `exp_neg_le_pow'`, `exp_neg_le_rpow'`
`table_14` 📖	CompOp	—
`table_14_margin` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`check_row_prop_of_bounds` 📖	mathematical	`BKLNW_app.table_8_ε` `RS_prime.c₀`	`check_row_prop`	—	—
`exp_neg_le_pow` 📖	mathematical	—	`exp_neg_one_ub`	—	—
`exp_neg_le_pow'` 📖	mathematical	—	`exp_neg_one_ub`	—	`exp_neg_le_pow`
`exp_neg_le_rpow` 📖	mathematical	—	`exp_neg_one_ub`	—	—
`exp_neg_le_rpow'` 📖	mathematical	—	`exp_neg_one_ub`	—	`exp_neg_le_rpow`
`rpow_le_of_pow_le` 📖	—	—	—	—	—
`table_14_check` 📖	mathematical	`table_14`	`check_row_prop`	—	`BKLNW_app.table_8_ε_le_of_row` `BKLNW_app.table_8_mem_20` `exp_neg_le_pow'` `exp_neg_le_rpow'` `rpow_le_of_pow_le` `check_row_prop_of_bounds` `BKLNW_app.table_8_mem_25` `BKLNW_app.table_8_mem_30` `BKLNW_app.table_8_mem_35` `BKLNW_app.table_8_mem_40` `LogTables.log_10_gt` `LogTables.log_10_lt` `BKLNW_app.table_8_mem_45` `BKLNW_app.table_8_mem_50` `BKLNW_app.table_8_mem_60` `BKLNW_app.table_8_mem_70` `BKLNW_app.table_8_mem_80` `BKLNW_app.table_8_mem_90` `BKLNW_app.table_8_mem_100` `BKLNW_app.table_8_mem_200` `BKLNW_app.table_8_mem_300` `BKLNW_app.table_8_mem_400` `BKLNW_app.table_8_mem_500` `BKLNW_app.table_8_mem_700` `BKLNW_app.table_8_mem_1000` `BKLNW_app.table_8_mem_2000` `BKLNW_app.table_8_mem_3000` `BKLNW_app.table_8_mem_4000` `BKLNW_app.table_8_mem_5000` `BKLNW_app.table_8_mem_7000` `BKLNW_app.table_8_mem_10000` `BKLNW_app.table_8_mem_11000` `BKLNW_app.table_8_mem_12000` `BKLNW_app.table_8_mem_13000` `BKLNW_app.table_8_mem_13800` `BKLNW_app.table_8_mem_15000` `BKLNW_app.table_8_mem_17000` `BKLNW_app.table_8_mem_20000` `BKLNW_app.table_8_mem_22000` `BKLNW_app.table_8_mem_25000`

---

← Back to Index