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 `zeroes_codiscreteWithin_compl_one`, `zeroes_on_Compact_finite`, `zeroes_on_Compact_finite'`, `zeroes_rect_disjoint₁`, `zeroes_rect_eq`, `zeroes_rect_union`, `riemannZeta_analyticOn_compl_one`, `riemannZeta_differentiableOn_compl_one`, `riemannZeta_eventually_ne_zero`, `riemannZeta_no_zeroes_near_one`, `bound`	11
Total	29

(root)

Definitions

Name	Category	Theorems
`zero_density_bound` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`riemannZeta_analyticOn_compl_one` 📖	—	—	—	—	`riemannZeta_differentiableOn_compl_one`
`riemannZeta_differentiableOn_compl_one` 📖	—	—	—	—	—
`riemannZeta_eventually_ne_zero` 📖	—	—	—	—	—
`riemannZeta_no_zeroes_near_one` 📖	—	—	—	—	`riemannZeta_eventually_ne_zero`

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	4 math math: `zeroes_rect_eq`, `zeroes_on_Compact_finite'`, `zeroes_codiscreteWithin_compl_one`, `zeroes_on_Compact_finite`
`zeroes_rect` 📖	CompOp	3 math math: `zeroes_rect_eq`, `zeroes_rect_union`, `zeroes_rect_disjoint₁`
`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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zeroes_codiscreteWithin_compl_one` 📖	mathematical	—	`zeroes`	—	`riemannZeta_analyticOn_compl_one`
`zeroes_on_Compact_finite` 📖	mathematical	—	`zeroes`	—	`riemannZeta_analyticOn_compl_one` `zeroes_codiscreteWithin_compl_one`
`zeroes_on_Compact_finite'` 📖	mathematical	—	`zeroes`	—	`riemannZeta_no_zeroes_near_one` `zeroes_on_Compact_finite`
`zeroes_rect_disjoint₁` 📖	mathematical	—	`zeroes_rect`	—	—
`zeroes_rect_eq` 📖	mathematical	—	`zeroes_rect` `zeroes`	—	—
`zeroes_rect_union` 📖	mathematical	—	`zeroes_rect`	—	—

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	2 math math: `bound`, `BKLNW_app.bklnw_eq_A_13`
`q` 📖	CompOp	2 math math: `bound`, `BKLNW_app.bklnw_eq_A_13`
`σ_range` 📖	CompOp	—

Theorems

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

---

← Back to Index