BKLNW

📁 Source: PrimeNumberTheoremAnd/BKLNW.lean

Statistics

Metric	Count
Definitions `Inputs`, `a₁`, `a₂`, `default`, `toPre_inputs`, `α`, `Pre_inputs`, `default`, `x₁`, `ε`, `Table_15`, `a₁`, `a₂`, `f`, `summand`, `table_cor_5_1`, `u`	17
Theorems `hα`, `epsilon_nonneg`, `hx₁`, `hx₁'`, `hε`, `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`	37
Total	54
⚠️ With sorry `prop_3_sub_1`, `thm_1b`, `thm_1b_table`	3

BKLNW

Definitions

Name	Category	Theorems
`Inputs` 📖	CompData	—
`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_cor_5_1` 📖	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
`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`	—	—
`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