FioriKadiriSwidinsky

📁 Source: PrimeNumberTheoremAnd/FioriKadiriSwidinsky.lean

Statistics

Metric	Count
Definitions `incomplete`, `A`, `Hn`, `Hσ`, `Inputs`, `B₀`, `B₁`, `H₀`, `R`, `RvM`, `S₀`, `T₀`, `ZDB`, `b₁`, `b₂`, `b₃`, `default`, `corollary_2_9`, `corollary_2_9_merged`, `Sigma`, `s₀`, `table_1`, `table_5`, `table_8`, `ε`, `ε₁`, `ε₂`, `ε₃`, `ε₄`, `σn`, `incomplete`	31
Theorems `FKS_corollary_1_3`, `FKS_corollary_1_4`, `hH₀`, `hR`, `hRvM`, `hS₀T₀`, `corollary_2_3`, `corollary_3_10`, `corollary_3_12`, `lemma_2_1`, `lemma_2_5`, `lemma_5_3`, `lemma_5_4`, `proposition_3_11`, `proposition_3_14`, `proposition_3_4`, `proposition_3_6`, `proposition_3_8`, `remark_2_6_a`, `remark_2_6_b`, `remark_3_7`, `Hσ_zeroes`, `table_1_prop`, `theorem_1_1`, `theorem_1_1b`, `theorem_1_2b`, `theorem_2_7`, `theorem_3_1`, `theorem_3_2`	29
Total	60
⚠️ With sorry `corollary_2_9_merged`, `FKS_corollary_1_3`, `FKS_corollary_1_4`, `corollary_2_3`, `corollary_3_10`, `corollary_3_12`, `lemma_2_1`, `lemma_2_5`, `lemma_5_3`, `lemma_5_4`, `proposition_3_11`, `proposition_3_14`, `proposition_3_4`, `proposition_3_6`, `proposition_3_8`, `remark_2_6_b`, `remark_3_7`, `Hσ_zeroes`, `table_1_prop`, `theorem_1_1`, `theorem_1_1b`, `theorem_1_2b`, `theorem_2_7`, `theorem_3_1`, `theorem_3_2`	25

Complex.Gamma

Definitions

Name	Category	Theorems
`incomplete` 📖	CompOp	—

FKS

Definitions

Name	Category	Theorems
`A` 📖	CompOp	2 math math: `FKS2.remark_15`, `theorem_1_2b`
`Hn` 📖	CompOp	—
`Hσ` 📖	CompOp	2 math math: `remark_3_7`, `riemannZeta.Hσ_zeroes`
`Inputs` 📖	CompData	—
`corollary_2_9` 📖	CompOp	—
`corollary_2_9_merged` 📖 ⚠️	CompOp	—
`s₀` 📖	CompOp	1 math math: `lemma_2_5`
`table_1` 📖	CompOp	—
`table_5` 📖	CompOp	—
`table_8` 📖	CompOp	—
`ε` 📖	CompOp	1 math math: `theorem_1_1`
`ε₁` 📖	CompOp	1 math math: `proposition_3_4`
`ε₂` 📖	CompOp	1 math math: `proposition_3_6`
`ε₃` 📖	CompOp	1 math math: `proposition_3_8`
`ε₄` 📖	CompOp	2 math math: `proposition_3_14`, `corollary_3_12`
`σn` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FKS_corollary_1_3` 📖 ⚠️	mathematical	—	`Eψ.classicalBound`	—	—
`FKS_corollary_1_4` 📖 ⚠️	mathematical	—	`Eψ.classicalBound`	—	—
`corollary_2_3` 📖 ⚠️	mathematical	`Inputs.T₀`	`riemannZeta.zeroes_sum` `Inputs.S₀` `Inputs.B₁`	—	—
`corollary_3_10` 📖 ⚠️	mathematical	—	`riemannZeta.Sigma`	—	—
`corollary_3_12` 📖 ⚠️	mathematical	`Hσ` `Inputs.H₀` `Inputs.R`	`riemannZeta.Sigma` `ε₄`	—	—
`lemma_2_1` 📖 ⚠️	mathematical	—	`riemannZeta.zeroes_sum` `Inputs.B₁`	—	—
`lemma_2_5` 📖 ⚠️	mathematical	`zero_density_bound.T₀` `Inputs.ZDB` `zero_density_bound.σ_range`	`s₀` `Inputs.B₀`	—	—
`lemma_5_3` 📖 ⚠️	mathematical	—	`Eψ`	—	—
`lemma_5_4` 📖 ⚠️	mathematical	—	`Eψ`	—	—
`proposition_3_11` 📖 ⚠️	mathematical	`Hσ` `Inputs.H₀` `Inputs.R`	`riemannZeta.Sigma` `riemannZeta.N'`	—	—
`proposition_3_14` 📖 ⚠️	mathematical	—	`ε₄` `zero_density_bound.c₁` `Inputs.ZDB` `Inputs.R`	—	—
`proposition_3_4` 📖 ⚠️	mathematical	—	`Eψ` `riemannZeta.zeroes_sum` `ε₁`	—	—
`proposition_3_6` 📖 ⚠️	mathematical	`Inputs.T₀`	`riemannZeta.Sigma` `ε₂`	—	—
`proposition_3_8` 📖 ⚠️	mathematical	`zero_density_bound.σ_range` `Inputs.ZDB` `Inputs.H₀`	`riemannZeta.Sigma` `ε₃`	—	—
`remark_2_6_a` 📖	mathematical	—	`Real.Gamma.incomplete`	—	—
`remark_2_6_b` 📖 ⚠️	mathematical	—	`Real.Gamma.incomplete`	—	—
`remark_3_7` 📖 ⚠️	mathematical	—	`Hσ`	—	—
`table_1_prop` 📖 ⚠️	mathematical	`table_1`	`riemannZeta.zeroes_sum`	—	—
`theorem_1_1` 📖 ⚠️	mathematical	—	`Eψ` `ε`	—	—
`theorem_1_1b` 📖 ⚠️	mathematical	`table_5`	`Eψ`	—	—
`theorem_1_2b` 📖 ⚠️	mathematical	—	`Eψ.classicalBound` `A`	—	—
`theorem_2_7` 📖 ⚠️	mathematical	`Inputs.H₀`	`riemannZeta.N'` `KLN.CC₁` `KLN.CC₂`	—	—
`theorem_3_1` 📖 ⚠️	mathematical	—	`Eψ` `riemannZeta.zeroes_sum`	—	—
`theorem_3_2` 📖 ⚠️	mathematical	—	`riemannZeta.zeroes_sum`	—	—

FKS.Inputs

Definitions

Name	Category	Theorems
`B₀` 📖	CompOp	1 math math: `FKS.lemma_2_5`
`B₁` 📖	CompOp	2 math math: `FKS.corollary_2_3`, `FKS.lemma_2_1`
`H₀` 📖	CompOp	1 math math: `hH₀`
`R` 📖	CompOp	2 math math: `FKS.proposition_3_14`, `hR`
`RvM` 📖	CompOp	—
`S₀` 📖	CompOp	2 math math: `hS₀T₀`, `FKS.corollary_2_3`
`T₀` 📖	CompOp	1 math math: `hS₀T₀`
`ZDB` 📖	CompOp	1 math math: `FKS.proposition_3_14`
`b₁` 📖	CompOp	1 math math: `hRvM`
`b₂` 📖	CompOp	1 math math: `hRvM`
`b₃` 📖	CompOp	1 math math: `hRvM`
`default` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hH₀` 📖	mathematical	—	`riemannZeta.RH_up_to` `H₀`	—	—
`hR` 📖	mathematical	—	`riemannZeta.classicalZeroFree` `R`	—	—
`hRvM` 📖	mathematical	—	`riemannZeta.Riemann_vonMangoldt_bound` `b₁` `b₂` `b₃`	—	—
`hS₀T₀` 📖	mathematical	—	`riemannZeta.zeroes_sum` `T₀` `S₀`	—	—

FKS.riemannZeta

Definitions

Name	Category	Theorems
`Sigma` 📖	CompOp	5 math math: `FKS.proposition_3_8`, `FKS.proposition_3_11`, `FKS.corollary_3_12`, `FKS.proposition_3_6`, `FKS.corollary_3_10`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Hσ_zeroes` 📖 ⚠️	mathematical	`riemannZeta.classicalZeroFree`	`riemannZeta.N'` `FKS.Hσ`	—	—

Real.Gamma

Definitions

Name	Category	Theorems
`incomplete` 📖	CompOp	2 math math: `FKS.remark_2_6_a`, `FKS.remark_2_6_b`

---

← Back to Index