FKS2

📁 Source: PrimeNumberTheoremAnd/FKS2.lean

Statistics

Metric	Count
Definitions `Table_4`, `Table_5`, `dawson`, `default_b`, `g_bound`, `table6`, `table7`, `δ`, `εθ_from_εψ`, `επ_num`, `μ_asymp`, `μ_num`, `μ_num_1`, `μ_num_2`, `ν_asymp`	15
Theorems `corollary_11`, `corollary_14`, `corollary_14_small_adm`, `corollary_21`, `corollary_22`, `corollary_23`, `corollary_24`, `corollary_26`, `corollary_8`, `hasDerivAt_Li`, `lemma_10_substep`, `lemma_10_substep_2`, `lemma_10a`, `lemma_10b`, `lemma_10c`, `lemma_12`, `lemma_19`, `lemma_20_a`, `lemma_20_b`, `proposition_13`, `proposition_17`, `psi_le_bound`, `psi_le_bound_large`, `psi_le_bound_medium`, `psi_le_bound_small`, `remark_15`, `remark_7`, `remark_after_corollary_11`, `theorem_3`, `theorem_6`, `theorem_6_1`, `theorem_6_2`, `theorem_6_3`, `theorem_6_alt`	34
Total	49
⚠️ With sorry `corollary_22`, `corollary_23`, `corollary_24`, `corollary_26`, `corollary_8`, `lemma_12`, `lemma_19`, `lemma_20_b`, `proposition_13`, `remark_15`, `remark_after_corollary_11`, `theorem_3`, `theorem_6`, `theorem_6_1`, `theorem_6_2`, `theorem_6_3`, `theorem_6_alt`	17

FKS2

Definitions

Name	Category	Theorems
`Table_4` 📖	CompOp	—
`Table_5` 📖	CompOp	—
`dawson` 📖	CompOp	2 math math: `remark_after_corollary_11`, `lemma_12`
`default_b` 📖	CompOp	—
`g_bound` 📖	CompOp	6 math math: `lemma_10_substep_2`, `lemma_10_substep`, `lemma_10a`, `lemma_10c`, `corollary_11`, `lemma_10b`
`table6` 📖	CompOp	—
`table7` 📖	CompOp	—
`δ` 📖	CompOp	—
`εθ_from_εψ` 📖	CompOp	1 math math: `proposition_17`
`επ_num` 📖	CompOp	2 math math: `theorem_6`, `corollary_8`
`μ_asymp` 📖	CompOp	2 math math: `theorem_3`, `corollary_21`
`μ_num` 📖	CompOp	—
`μ_num_1` 📖	CompOp	1 math math: `remark_7`
`μ_num_2` 📖	CompOp	2 math math: `remark_7`, `theorem_6_alt`
`ν_asymp` 📖	CompOp	2 math math: `corollary_21`, `proposition_13`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`corollary_11` 📖	mathematical	—	`g_bound`	—	`lemma_10a`
`corollary_14` 📖	mathematical	—	`Eθ.classicalBound`	—	`corollary_14_small_adm` `LogTables.log_2_lt` `LogTables.log_2_gt` `LogTables.log_10_gt` `BKLNW_app.table_8_ε_le_of_row` `BKLNW_app.table_8_mem_40` `LogTables.log_13_gt` `FKS.FKS_corollary_1_3` `proposition_13` `Eθ.classicalBound.eq_1` `BKLNW.buthe_eq_1_7`
`corollary_14_small_adm` 📖	mathematical	—	`admissible_bound`	—	`LogTables.log_2_gt` `LogTables.log_5_gt` `LogTables.log_23_gt`
`corollary_21` 📖	mathematical	`Eψ.classicalBound`	`Eπ` `admissible_bound` `ν_asymp` `μ_asymp`	—	`theorem_3` `proposition_13`
`corollary_22` 📖 ⚠️	mathematical	—	`Eπ.classicalBound`	—	—
`corollary_23` 📖 ⚠️	mathematical	`table6`	`Eπ.classicalBound`	—	—
`corollary_24` 📖 ⚠️	mathematical	`table7`	`Eπ`	—	—
`corollary_26` 📖 ⚠️	mathematical	—	`Eπ.bound`	—	—
`corollary_8` 📖 ⚠️	mathematical	`Eθ.numericalBound`	`Eπ` `επ_num`	—	—
`hasDerivAt_Li` 📖	mathematical	—	`Li`	—	—
`lemma_10_substep` 📖	mathematical	—	`g_bound`	—	—
`lemma_10_substep_2` 📖	mathematical	—	`g_bound`	—	`lemma_10_substep`
`lemma_10a` 📖	mathematical	—	`g_bound`	—	`lemma_10_substep_2`
`lemma_10b` 📖	mathematical	—	`g_bound`	—	`lemma_10_substep_2`
`lemma_10c` 📖	mathematical	—	`g_bound`	—	—
`lemma_12` 📖 ⚠️	mathematical	`Eθ.classicalBound`	`Eθ` `dawson`	—	—
`lemma_19` 📖 ⚠️	mathematical	`Eθ.numericalBound`	`Li`	—	—
`lemma_20_a` 📖	mathematical	—	`Li`	—	`hasDerivAt_Li`
`lemma_20_b` 📖 ⚠️	mathematical	—	`Li`	—	—
`proposition_13` 📖 ⚠️	mathematical	`Eψ.classicalBound`	`Eθ.classicalBound` `ν_asymp`	—	—
`proposition_17` 📖	mathematical	`Eψ`	`εθ_from_εψ`	—	`CostaPereira.theorem_1a` `psi_le_bound` `εθ_from_εψ.eq_1`
`psi_le_bound` 📖	—	—	—	—	`psi_le_bound_small` `psi_le_bound_medium` `psi_le_bound_large`
`psi_le_bound_large` 📖	—	—	—	—	`BKLNW_app.theorem_2` `LogTables.log_10_gt` `LogTables.log_10_lt` `BKLNW_app.table_8_ε.le_simp`
`psi_le_bound_medium` 📖	—	—	—	—	`BKLNW_app.bklnw_eq_A_26`
`psi_le_bound_small` 📖	—	—	—	—	—
`remark_15` 📖 ⚠️	mathematical	—	`Eθ.classicalBound` `FKS.A`	—	—
`remark_7` 📖	mathematical	—	`μ_num_1` `μ_num_2`	—	`hasDerivAt_Li` `theorem_6_2`
`remark_after_corollary_11` 📖 ⚠️	mathematical	—	`dawson`	—	—
`theorem_3` 📖 ⚠️	mathematical	`Eθ.classicalBound`	`Eπ.classicalBound` `μ_asymp`	—	—
`theorem_6` 📖 ⚠️	mathematical	`Eθ.numericalBound`	`Eπ` `επ_num`	—	—
`theorem_6_1` 📖 ⚠️	mathematical	`Eθ.numericalBound`	`Eπ` `Eθ` `Li`	—	—
`theorem_6_2` 📖 ⚠️	—	—	—	—	—
`theorem_6_3` 📖 ⚠️	mathematical	—	`Li`	—	—
`theorem_6_alt` 📖 ⚠️	mathematical	`Eθ.numericalBound`	`Eπ` `μ_num_2`	—	—

---

← Back to Index