Documentation Verification Report

BKLNW_app

📁 Source: PrimeNumberTheoremAnd/BKLNW_app.lean

Statistics

Metric	Count
Definitions `Inputs`, `A`, `B`, `C`, `H`, `R`, `ZDB`, `c3`, `c4`, `c5`, `default`, `k`, `s₂`, `Sigma₁`, `Sigma₂`, `bklnw_eq_A_8`, `pre_μ`, `s₁`, `η`, `μ`, `ν`, `ℓ`	22
Theorems `hH`, `hR`, `bklnw_cor_15_1`, `bklnw_cor_15_1'`, `bklnw_eq_A_10`, `bklnw_eq_A_12`, `bklnw_eq_A_13`, `bklnw_eq_A_26`, `bklnw_eq_A_7`, `bklnw_eq_A_9`, `bklnw_lemma_15`, `bklnw_thm_15`, `bklnw_thm_16`, `theorem_2`, `thm_14`	15
Total	37
⚠️ With sorry `bklnw_eq_A_10`, `bklnw_eq_A_12`, `bklnw_eq_A_7`, `bklnw_thm_15`, `bklnw_thm_16`, `theorem_2`, `thm_14`	7

BKLNW_app

Definitions

Name	Category	Theorems
`Inputs` 📖	CompData	—
`Sigma₁` 📖	CompOp	2 math math: `bklnw_eq_A_10`, `bklnw_eq_A_9`
`Sigma₂` 📖	CompOp	3 math math: `bklnw_eq_A_12`, `bklnw_eq_A_9`, `bklnw_eq_A_13`
`bklnw_eq_A_8` 📖	CompOp	1 math math: `bklnw_thm_15`
`pre_μ` 📖	CompOp	—
`s₁` 📖	CompOp	1 math math: `bklnw_thm_15`
`η` 📖	CompOp	—
`μ` 📖	CompOp	1 math math: `bklnw_thm_16`
`ν` 📖	CompOp	1 math math: `bklnw_thm_16`
`ℓ` 📖	CompOp	1 math math: `bklnw_thm_16`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bklnw_cor_15_1` 📖	mathematical	`Eψ`	`Eψ`	—	`bklnw_lemma_15` `Buthe.theorem_2a`
`bklnw_cor_15_1'` 📖	mathematical	—	`Eψ` `table_8_margin`	—	`bklnw_cor_15_1` `Eψ.eq_1` `theorem_2` `LogTables.log_10_gt` `LogTables.log_10_lt` `table_8_ε.le_simp`
`bklnw_eq_A_10` 📖 ⚠️	mathematical	—	`Sigma₁`	—	—
`bklnw_eq_A_12` 📖 ⚠️	mathematical	`Inputs.H` `zero_density_bound.σ_range` `Inputs.ZDB` `zero_density_bound.T₀`	`Sigma₂` `Inputs.H` `Inputs.R` `zero_density_bound.N` `Inputs.ZDB`	—	—
`bklnw_eq_A_13` 📖	mathematical	`Inputs.H` `zero_density_bound.σ_range` `Inputs.ZDB` `zero_density_bound.T₀`	`Sigma₂` `Inputs.H` `Inputs.R` `zero_density_bound.c₁` `Inputs.ZDB` `zero_density_bound.p` `zero_density_bound.q` `zero_density_bound.c₂`	—	`bklnw_eq_A_12`
`bklnw_eq_A_26` 📖	mathematical	—	`Eψ`	—	`Buthe.theorem_2a`
`bklnw_eq_A_7` 📖 ⚠️	mathematical	—	`riemannZeta.zeroes_sum`	—	—
`bklnw_eq_A_9` 📖	mathematical	—	`riemannZeta.zeroes_sum` `Sigma₁` `Sigma₂`	—	`riemannZeta.zeroes_rect_disjoint₁` `riemannZeta.zeroes_rect_eq` `riemannZeta.zeroes_on_Compact_finite'` `riemannZeta.zeroes_rect_union`
`bklnw_lemma_15` 📖	mathematical	`Eψ`	`Eψ`	—	—
`bklnw_thm_15` 📖 ⚠️	mathematical	`Inputs.H`	`bklnw_eq_A_8` `s₁` `Inputs.s₂` `Inputs.H`	—	—
`bklnw_thm_16` 📖 ⚠️	mathematical	`ν` `μ`	`Eψ` `ν` `μ` `riemannZeta.zeroes_sum` `ℓ`	—	—
`theorem_2` 📖 ⚠️	mathematical	—	`table_8_ε`	—	—
`thm_14` 📖 ⚠️	mathematical	—	`Eψ` `Inputs.A` `Inputs.R` `Inputs.B` `Inputs.C`	—	—

BKLNW_app.Inputs

Definitions

Name	Category	Theorems
`A` 📖	CompOp	1 math math: `BKLNW_app.thm_14`
`B` 📖	CompOp	1 math math: `BKLNW_app.thm_14`
`C` 📖	CompOp	1 math math: `BKLNW_app.thm_14`
`H` 📖	CompOp	4 math math: `hH`, `BKLNW_app.bklnw_eq_A_12`, `BKLNW_app.bklnw_thm_15`, `BKLNW_app.bklnw_eq_A_13`
`R` 📖	CompOp	4 math math: `BKLNW_app.thm_14`, `BKLNW_app.bklnw_eq_A_12`, `hR`, `BKLNW_app.bklnw_eq_A_13`
`ZDB` 📖	CompOp	2 math math: `BKLNW_app.bklnw_eq_A_12`, `BKLNW_app.bklnw_eq_A_13`
`c3` 📖	CompOp	—
`c4` 📖	CompOp	—
`c5` 📖	CompOp	—
`default` 📖	CompOp	—
`k` 📖	CompOp	—
`s₂` 📖	CompOp	1 math math: `BKLNW_app.bklnw_thm_15`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hH` 📖	mathematical	—	`riemannZeta.RH_up_to` `H`	—	—
`hR` 📖	mathematical	—	`riemannZeta.classicalZeroFree` `R`	—	—

---

← Back to Index