BKLNW

📁 Source: PrimeNumberTheoremAnd/BKLNW.lean

Statistics

Metric	Count
Definitions `B`, `B_8_1`, `B_8_1'`, `Btilde`, `C_bk`, `Inputs`, `a₁`, `a₂`, `default`, `toPre_inputs`, `α`, `K`, `Pre_inputs`, `default`, `x₁`, `ε`, `Table_15`, `a₁`, `a₂`, `f`, `summand`, `table_10_bs`, `table_10_next`, `table_cor_5_1`, `table_from_buthe`, `u`	26
Theorems `hα`, `epsilon_nonneg`, `hx₁`, `hx₁'`, `hε`, `bklnw_cor_8_1a`, `bklnw_cor_8_1b`, `bklnw_corollary_9_1`, `bklnw_corollary_9_1_explicit`, `bklnw_eq_3_11`, `bklnw_eq_3_17`, `bklnw_eq_3_18`, `bklnw_lemma_8`, `bklnw_lemma_9`, `bklnw_table_10_verification`, `bklnw_table_11_verification`, `bklnw_table_12_verification`, `bklnw_table_from_buthe`, `buthe_eq_1_7`, `cor_14_1`, `cor_2_1`, `cor_3_1`, `cor_5_1`, `g_decreasing_interval`, `lem_6`, `lemma_11a`, `lemma_11b`, `prop_3`, `prop_3_sub_1`, `prop_3_sub_2`, `prop_3_sub_3`, `prop_3_sub_4`, `prop_3_sub_5`, `prop_3_sub_6`, `prop_3_sub_7`, `prop_3_sub_8`, `prop_4_a`, `prop_4_b`, `sum_gt`, `aux`, `summand_mono`, `summand_pos`, `aux`, `thm_1a`, `thm_1a_crit`, `thm_1a_table`, `thm_1b`, `thm_1b_table`, `thm_5`, `u_diff_factored`	50
Total	76
⚠️ With sorry `bklnw_cor_8_1a`, `bklnw_cor_8_1b`, `bklnw_corollary_9_1`, `bklnw_corollary_9_1_explicit`, `bklnw_eq_3_11`, `bklnw_eq_3_17`, `bklnw_eq_3_18`, `bklnw_lemma_8`, `bklnw_lemma_9`, `bklnw_table_10_verification`, `bklnw_table_11_verification`, `bklnw_table_12_verification`, `bklnw_table_from_buthe`, `thm_1b`, `thm_1b_table`	15

BKLNW

Definitions

Name	Category	Theorems
`B` 📖	CompOp	2 math math: `bklnw_eq_3_11`, `bklnw_lemma_8`
`B_8_1` 📖	CompOp	2 math math: `bklnw_table_10_verification`, `bklnw_cor_8_1a`
`B_8_1'` 📖	CompOp	2 math math: `bklnw_cor_8_1b`, `bklnw_table_11_verification`
`Btilde` 📖	CompOp	1 math math: `bklnw_eq_3_11`
`C_bk` 📖	CompOp	2 math math: `bklnw_corollary_9_1`, `bklnw_table_12_verification`
`Inputs` 📖	CompData	—
`K` 📖	CompOp	—
`Pre_inputs` 📖	CompData	—
`Table_15` 📖	CompOp	—
`a₁` 📖	CompOp	2 math math: `cor_14_1`, `cor_5_1`
`a₂` 📖	CompOp	4 math math: `cor_5_1_rem'`, `cor_5_1_rem`, `cor_14_1`, `cor_5_1`
`f` 📖	CompOp	20 math math: `prop_3_sub_3`, `a2_43_mem_Icc`, `a2_40_mem_Icc`, `a2_30_mem_Icc`, `prop_3_sub_2`, `prop_3_sub_1`, `prop_3_sub_6`, `a2_150_mem_Icc`, `prop_3_sub_7`, `a2_20_mem_Icc`, `a2_35_mem_Icc`, `a2_25_mem_Icc`, `a2_250_mem_Icc`, `a2_100_mem_Icc`, `prop_3_sub_8`, `a2_300_mem_Icc`, `a2_200_mem_Icc`, `prop_3_sub_5`, `prop_3`, `cor_3_1`
`summand` 📖	CompOp	5 math math: `summand_pos`, `summand_mono`, `sum_gt.aux`, `u_diff_factored`, `sum_gt`
`table_10_bs` 📖	CompOp	—
`table_10_next` 📖	CompOp	1 math math: `bklnw_table_10_verification`
`table_cor_5_1` 📖	CompOp	—
`table_from_buthe` 📖	CompOp	—
`u` 📖	CompOp	3 math math: `prop_3_sub_3`, `prop_3_sub_4`, `u_diff_factored`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bklnw_cor_8_1a` 📖 ⚠️	mathematical	—	`B_8_1`	—	—
`bklnw_cor_8_1b` 📖 ⚠️	mathematical	`K`	`B_8_1'`	—	—
`bklnw_corollary_9_1` 📖 ⚠️	mathematical	`table_from_buthe`	`C_bk` `RS_prime.c₀`	—	—
`bklnw_corollary_9_1_explicit` 📖 ⚠️	—	`table_12`	—	—	—
`bklnw_eq_3_11` 📖 ⚠️	mathematical	—	`B` `Btilde`	—	—
`bklnw_eq_3_17` 📖 ⚠️	—	—	—	—	—
`bklnw_eq_3_18` 📖 ⚠️	—	—	—	—	—
`bklnw_lemma_8` 📖 ⚠️	mathematical	—	`B`	—	—
`bklnw_lemma_9` 📖 ⚠️	—	—	—	—	—
`bklnw_table_10_verification` 📖 ⚠️	mathematical	`table_10`	`B_8_1` `table_10_next`	—	—
`bklnw_table_11_verification` 📖 ⚠️	mathematical	`table_11`	`B_8_1'`	—	—
`bklnw_table_12_verification` 📖 ⚠️	mathematical	`table_12`	`C_bk` `RS_prime.c₀`	—	—
`bklnw_table_from_buthe` 📖 ⚠️	—	`table_from_buthe`	—	—	—
`buthe_eq_1_7` 📖	—	—	—	—	`Buthe.theorem_2c`
`cor_14_1` 📖	mathematical	`Eψ.classicalBound`	`Eθ` `admissible_bound` `a₁` `a₂`	—	`Pre_inputs.epsilon_nonneg` `cor_5_1`
`cor_2_1` 📖	mathematical	—	`BKLNW_app.table_8_margin`	—	`buthe_eq_1_7` `LogTables.log_10_gt` `LogTables.log_10_lt` `BKLNW_app.theorem_2` `BKLNW_app.table_8_ε.le_simp` `thm_1a`
`cor_3_1` 📖	mathematical	—	`Inputs.α` `f`	—	`prop_3` `Inputs.hα`
`cor_5_1` 📖	mathematical	—	`a₁` `a₂`	—	`thm_5`
`g_decreasing_interval` 📖	—	—	—	—	—
`lem_6` 📖	mathematical	`Eθ.classicalBound`	`Eθ`	—	`g_decreasing_interval`
`lemma_11a` 📖	mathematical	—	`Pre_inputs.ε` `Pre_inputs.x₁`	—	`Pre_inputs.hx₁` `Pre_inputs.hx₁'` `Pre_inputs.epsilon_nonneg` `Pre_inputs.hε`
`lemma_11b` 📖	mathematical	—	`Pre_inputs.ε` `RS_prime.c₀`	—	`RS_prime.theorem_12`
`prop_3` 📖	mathematical	—	`Inputs.α` `f`	—	`Inputs.hα` `prop_3_sub_8`
`prop_3_sub_1` 📖	mathematical	—	`Inputs.α` `f`	—	`Inputs.hα`
`prop_3_sub_2` 📖	mathematical	—	`f`	—	—
`prop_3_sub_3` 📖	mathematical	—	`f` `u`	—	`f.eq_1` `u.eq_1`
`prop_3_sub_4` 📖	mathematical	—	`u`	—	`u_diff_factored` `sum_gt`
`prop_3_sub_5` 📖	mathematical	—	`f`	—	`prop_3_sub_3` `prop_3_sub_4`
`prop_3_sub_6` 📖	mathematical	—	`f`	—	`prop_3_sub_2` `prop_3_sub_5`
`prop_3_sub_7` 📖	mathematical	—	`f`	—	`prop_3_sub_2`
`prop_3_sub_8` 📖	mathematical	—	`f`	—	`prop_3_sub_7` `prop_3_sub_6`
`prop_4_a` 📖	mathematical	—	`Pre_inputs.ε` `Inputs.toPre_inputs` `Pre_inputs.x₁`	—	`Pre_inputs.hx₁` `Pre_inputs.hx₁'` `Pre_inputs.epsilon_nonneg` `Pre_inputs.hε`
`prop_4_b` 📖	mathematical	—	`Pre_inputs.ε` `Inputs.toPre_inputs`	—	`Pre_inputs.hε`
`sum_gt` 📖	mathematical	—	`summand`	—	`sum_gt.aux` `summand_pos` `summand_mono`
`summand_mono` 📖	mathematical	—	`summand`	—	`summand_pos.aux`
`summand_pos` 📖	mathematical	—	`summand`	—	`summand_pos.aux`
`thm_1a` 📖	mathematical	—	`Pre_inputs.ε` `Pre_inputs.default` `RS_prime.c₀`	—	`BKLNW_app.theorem_2`
`thm_1a_crit` 📖	—	`check_row_prop`	—	—	`thm_1a`
`thm_1a_table` 📖	—	`table_14`	—	—	`thm_1a_crit` `table_14_check`
`thm_1b` 📖 ⚠️	—	—	—	—	—
`thm_1b_table` 📖 ⚠️	—	`Table_15`	—	—	—
`thm_5` 📖	mathematical	—	`Inputs.a₁` `Inputs.a₂`	—	`prop_4_a` `prop_4_b` `cor_3_1`
`u_diff_factored` 📖	mathematical	—	`u` `summand`	—	`u.eq_1` `summand.eq_1`

BKLNW.Inputs

Definitions

Name	Category	Theorems
`a₁` 📖	CompOp	1 math math: `BKLNW.thm_5`
`a₂` 📖	CompOp	1 math math: `BKLNW.thm_5`
`default` 📖	CompOp	—
`toPre_inputs` 📖	CompOp	2 math math: `BKLNW.prop_4_a`, `BKLNW.prop_4_b`
`α` 📖	CompOp	4 math math: `BKLNW.prop_3_sub_1`, `hα`, `BKLNW.prop_3`, `BKLNW.cor_3_1`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hα` 📖	mathematical	—	`α`	—	—

BKLNW.Pre_inputs

Definitions

Name	Category	Theorems
`default` 📖	CompOp	1 math math: `BKLNW.thm_1a`
`x₁` 📖	CompOp	3 math math: `hx₁`, `BKLNW.prop_4_a`, `BKLNW.lemma_11a`
`ε` 📖	CompOp	7 math math: `epsilon_nonneg`, `hε`, `BKLNW.prop_4_a`, `BKLNW.lemma_11b`, `BKLNW.lemma_11a`, `BKLNW.thm_1a`, `BKLNW.prop_4_b`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epsilon_nonneg` 📖	mathematical	—	`ε`	—	`hε`
`hx₁` 📖	mathematical	—	`x₁`	—	—
`hx₁'` 📖	—	`x₁`	—	—	—
`hε` 📖	mathematical	—	`ε`	—	—

BKLNW.sum_gt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aux` 📖	mathematical	—	`BKLNW.summand`	—	—

BKLNW.summand_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aux` 📖	—	—	—	—	—

---

← Back to Index