BKLNW_app_tables

📁 Source: PrimeNumberTheoremAnd/BKLNW_app_tables.lean

Statistics

Metric	Count
Definitions `table_8`, `table_8_margin`, `table_8_ε`, `table_8_ε'`	4
Theorems `le_of_not_lt`, `table_8_mem_100`, `table_8_mem_1000`, `table_8_mem_10000`, `table_8_mem_10500`, `table_8_mem_11000`, `table_8_mem_11500`, `table_8_mem_12000`, `table_8_mem_12500`, `table_8_mem_13000`, `table_8_mem_13500`, `table_8_mem_13800`, `table_8_mem_14000`, `table_8_mem_1500`, `table_8_mem_15000`, `table_8_mem_16000`, `table_8_mem_17000`, `table_8_mem_18000`, `table_8_mem_19000`, `table_8_mem_20`, `table_8_mem_200`, `table_8_mem_2000`, `table_8_mem_20000`, `table_8_mem_21`, `table_8_mem_21000`, `table_8_mem_22`, `table_8_mem_22000`, `table_8_mem_23`, `table_8_mem_23000`, `table_8_mem_24`, `table_8_mem_24000`, `table_8_mem_25`, `table_8_mem_2500`, `table_8_mem_25000`, `table_8_mem_30`, `table_8_mem_300`, `table_8_mem_3000`, `table_8_mem_35`, `table_8_mem_3500`, `table_8_mem_40`, `table_8_mem_400`, `table_8_mem_4000`, `table_8_mem_45`, `table_8_mem_4500`, `table_8_mem_50`, `table_8_mem_500`, `table_8_mem_5000`, `table_8_mem_5500`, `table_8_mem_60`, `table_8_mem_600`, `table_8_mem_6000`, `table_8_mem_6500`, `table_8_mem_70`, `table_8_mem_700`, `table_8_mem_7000`, `table_8_mem_7500`, `table_8_mem_80`, `table_8_mem_800`, `table_8_mem_8000`, `table_8_mem_8500`, `table_8_mem_90`, `table_8_mem_900`, `table_8_mem_9000`, `table_8_mem_9500`, `le_simp`, `table_8_ε_le_of_row`	66
Total	70

BKLNW_app

Definitions

Name	Category	Theorems
`table_8` 📖	CompOp	63 math math: `table_8_mem_21000`, `table_8_mem_6000`, `table_8_mem_23000`, `table_8_mem_24`, `table_8_mem_20`, `table_8_mem_18000`, `table_8_mem_21`, `table_8_mem_30`, `table_8_mem_700`, `table_8_mem_3000`, `table_8_mem_9000`, `table_8_mem_35`, `table_8_mem_10000`, `table_8_mem_17000`, `table_8_mem_300`, `table_8_mem_11000`, `table_8_mem_12000`, `table_8_mem_22000`, `table_8_mem_15000`, `table_8_mem_5000`, `table_8_mem_60`, `table_8_mem_22`, `table_8_mem_7000`, `table_8_mem_200`, `table_8_mem_20000`, `table_8_mem_25`, `table_8_mem_19000`, `table_8_mem_5500`, `table_8_mem_4000`, `table_8_mem_2500`, `table_8_mem_13800`, `table_8_mem_16000`, `table_8_mem_80`, `table_8_mem_900`, `table_8_mem_13500`, `table_8_mem_40`, `table_8_mem_70`, `table_8_mem_10500`, `table_8_mem_9500`, `table_8_mem_100`, `table_8_mem_25000`, `table_8_mem_13000`, `table_8_mem_8500`, `table_8_mem_7500`, `table_8_mem_3500`, `table_8_mem_12500`, `table_8_mem_8000`, `table_8_mem_14000`, `table_8_mem_23`, `table_8_mem_11500`, `table_8_mem_1000`, `table_8_mem_45`, `table_8_mem_400`, `table_8_mem_1500`, `table_8_mem_24000`, `table_8_mem_90`, `table_8_mem_6500`, `table_8_mem_50`, `table_8_mem_2000`, `table_8_mem_500`, `table_8_mem_800`, `table_8_mem_4500`, `table_8_mem_600`
`table_8_margin` 📖	CompOp	2 math math: `bklnw_cor_15_1'`, `BKLNW.cor_2_1`
`table_8_ε` 📖	CompOp	3 math math: `table_8_ε.le_simp`, `theorem_2`, `table_8_ε_le_of_row`
`table_8_ε'` 📖	CompOp	1 math math: `table_8_ε.le_simp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_of_not_lt` 📖	—	—	—	—	—
`table_8_mem_100` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_1000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_10000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_10500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_11000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_11500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_12000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_12500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_13000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_13500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_13800` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_14000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_1500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_15000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_16000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_17000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_18000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_19000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_20` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_200` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_2000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_20000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_21` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_21000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_22` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_22000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_23` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_23000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_24` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_24000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_25` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_2500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_25000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_30` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_300` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_3000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_35` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_3500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_40` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_400` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_4000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_45` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_4500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_50` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_5000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_5500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_60` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_600` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_6000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_6500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_70` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_700` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_7000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_7500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_80` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_800` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_8000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_8500` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_90` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_900` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_9000` 📖	mathematical	—	`table_8`	—	—
`table_8_mem_9500` 📖	mathematical	—	`table_8`	—	—
`table_8_ε_le_of_row` 📖	mathematical	`table_8`	`table_8_ε`	—	—

BKLNW_app.table_8_ε

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_simp` 📖	mathematical	—	`BKLNW_app.table_8_ε` `BKLNW_app.table_8_ε'`	—	`BKLNW_app.table_8_ε_le_of_row` `BKLNW_app.table_8_mem_20` `BKLNW_app.le_of_not_lt` `BKLNW_app.table_8_mem_21` `BKLNW_app.table_8_mem_22` `BKLNW_app.table_8_mem_23` `BKLNW_app.table_8_mem_24` `BKLNW_app.table_8_mem_25` `BKLNW_app.table_8_mem_30` `BKLNW_app.table_8_mem_35` `BKLNW_app.table_8_mem_40` `BKLNW_app.table_8_mem_45` `BKLNW_app.table_8_mem_50` `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_600` `BKLNW_app.table_8_mem_700` `BKLNW_app.table_8_mem_800` `BKLNW_app.table_8_mem_900` `BKLNW_app.table_8_mem_1000` `BKLNW_app.table_8_mem_1500` `BKLNW_app.table_8_mem_2000` `BKLNW_app.table_8_mem_2500` `BKLNW_app.table_8_mem_3000` `BKLNW_app.table_8_mem_3500` `BKLNW_app.table_8_mem_4000` `BKLNW_app.table_8_mem_4500` `BKLNW_app.table_8_mem_5000` `BKLNW_app.table_8_mem_5500` `BKLNW_app.table_8_mem_6000` `BKLNW_app.table_8_mem_6500` `BKLNW_app.table_8_mem_7000` `BKLNW_app.table_8_mem_7500` `BKLNW_app.table_8_mem_8000` `BKLNW_app.table_8_mem_8500` `BKLNW_app.table_8_mem_9000` `BKLNW_app.table_8_mem_9500` `BKLNW_app.table_8_mem_10000` `BKLNW_app.table_8_mem_10500` `BKLNW_app.table_8_mem_11000` `BKLNW_app.table_8_mem_11500` `BKLNW_app.table_8_mem_12000` `BKLNW_app.table_8_mem_12500` `BKLNW_app.table_8_mem_13000` `BKLNW_app.table_8_mem_13500` `BKLNW_app.table_8_mem_14000` `BKLNW_app.table_8_mem_15000` `BKLNW_app.table_8_mem_16000` `BKLNW_app.table_8_mem_17000` `BKLNW_app.table_8_mem_18000` `BKLNW_app.table_8_mem_19000` `BKLNW_app.table_8_mem_20000` `BKLNW_app.table_8_mem_21000` `BKLNW_app.table_8_mem_22000` `BKLNW_app.table_8_mem_23000` `BKLNW_app.table_8_mem_24000` `BKLNW_app.table_8_mem_25000`

---

← Back to Index