Documentation Verification Report

ZetaDefinitions

📁 Source: PrimeNumberTheoremAnd/ZetaDefinitions.lean

Statistics

Metric	Count
Definitions `N`, `N'`, `RH_up_to`, `Riemann_vonMangoldt_bound`, `RvM`, `classicalZeroFree`, `order`, `zeroes`, `zeroes_rect`, `zeroes_sum`, `zero_density_bound`, `N`, `T₀`, `c₁`, `c₂`, `p`, `q`, `σ_range`	18
Theorems `bound`	1
Total	19

(root)

Definitions

Name	Category	Theorems
`zero_density_bound` 📖	CompData	—

riemannZeta

Definitions

Name	Category	Theorems
`N` 📖	CompOp	—
`N'` 📖	CompOp	4 math math: `FKS.proposition_3_11`, `FKS.theorem_2_7`, `zero_density_bound.bound`, `FKS.riemannZeta.Hσ_zeroes`
`RH_up_to` 📖	MathDef	5 math math: `PT_theorem_1`, `GW_theorem`, `BKLNW_app.Inputs.hH`, `FKS.Inputs.hH₀`, `Platt_theorem`
`Riemann_vonMangoldt_bound` 📖	MathDef	3 math math: `FKS.Inputs.hRvM`, `RS.theorem_19`, `HSW.main_theorem`
`RvM` 📖	CompOp	—
`classicalZeroFree` 📖	MathDef	4 math math: `MTY_theorem`, `MT_theorem_1`, `BKLNW_app.Inputs.hR`, `FKS.Inputs.hR`
`order` 📖	CompOp	—
`zeroes` 📖	CompOp	—
`zeroes_rect` 📖	CompOp	—
`zeroes_sum` 📖	CompOp	10 math math: `BKLNW_app.bklnw_eq_A_7`, `BKLNW_app.bklnw_thm_16`, `FKS.theorem_3_2`, `FKS.Inputs.hS₀T₀`, `FKS.corollary_2_3`, `BKLNW_app.bklnw_eq_A_9`, `FKS.proposition_3_4`, `FKS.theorem_3_1`, `FKS.table_1_prop`, `FKS.lemma_2_1`

zero_density_bound

Definitions

Name	Category	Theorems
`N` 📖	CompOp	1 math math: `BKLNW_app.bklnw_eq_A_12`
`T₀` 📖	CompOp	—
`c₁` 📖	CompOp	3 math math: `FKS.proposition_3_14`, `bound`, `BKLNW_app.bklnw_eq_A_13`
`c₂` 📖	CompOp	2 math math: `bound`, `BKLNW_app.bklnw_eq_A_13`
`p` 📖	CompOp	1 math math: `bound`
`q` 📖	CompOp	1 math math: `bound`
`σ_range` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bound` 📖	mathematical	`T₀` `σ_range`	`riemannZeta.N'` `c₁` `p` `q` `c₂`	—	—

---

← Back to Index