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 `Eθ_eq_abs`, `Eθ_nonneg`, `Li_identity`, `Li_identity'`, `admissible_bound_le_0826`, `admissible_bound_mul`, `admissible_bound_pos`, `corollary_11`, `corollary_14`, `corollary_14_small_adm`, `corollary_21`, `corollary_22`, `corollary_23`, `corollary_24`, `corollary_26`, `corollary_8`, `corollary_8_apply_theorem_6`, `dawson_antitoneOn`, `dawson_mono_ge_one`, `dawson_nonneg`, `delta_nonneg`, `delta_term_bound`, `ereal_exp_ge_max`, `ereal_exp_toReal_le`, `ereal_toReal_coe_log`, `ereal_toReal_sub_mono`, `find_ereal_bin`, `h_monotoneOn`, `hasDerivAt_Li`, `hasDerivAt_Li_sub_div_log`, `he`, `integral_algebra`, `integral_one_div_log_sq`, `integral_term_bound`, `l0`, `l1`, `l2`, `l3`, `lemma_10_substep`, `lemma_10_substep_2`, `lemma_10a`, `lemma_10b`, `lemma_10c`, `lemma_12`, `lemma_19`, `lemma_20_a`, `lemma_20_b`, `logx_over_x_bound`, `m_simplify`, `proposition_13`, `proposition_17`, `psi_le_bound`, `psi_le_bound_large`, `psi_le_bound_medium`, `psi_le_bound_small`, `ratio_eq_g`, `ratio_mono`, `remark_15`, `remark_7`, `remark_after_corollary_11`, `sqrt_exp_le_half`, `sqrt_log_minus_ge_one`, `table6_mem`, `theorem_3`, `theorem_3_easy_preconditions`, `theorem_6`, `theorem_6_1`, `theorem_6_2`, `theorem_6_3`, `theorem_6_alt`	70
Total	85
⚠️ With sorry `corollary_22`, `corollary_23`, `corollary_24`, `lemma_20_b`, `proposition_13`, `remark_15`, `remark_after_corollary_11`, `theorem_6`, `theorem_6_1`, `theorem_6_2`	10

FKS2

Definitions

Name	Category	Theorems
`Table_4` 📖	CompOp	—
`Table_5` 📖	CompOp	—
`dawson` 📖	CompOp	6 math math: `dawson_mono_ge_one`, `remark_after_corollary_11`, `integral_term_bound`, `dawson_nonneg`, `lemma_12`, `dawson_antitoneOn`
`default_b` 📖	CompOp	—
`g_bound` 📖	CompOp	7 math math: `ratio_eq_g`, `lemma_10_substep_2`, `lemma_10_substep`, `lemma_10a`, `lemma_10c`, `corollary_11`, `lemma_10b`
`table6` 📖	CompOp	1 math math: `table6_mem`
`table7` 📖	CompOp	—
`δ` 📖	CompOp	2 math math: `delta_term_bound`, `delta_nonneg`
`εθ_from_εψ` 📖	CompOp	1 math math: `proposition_17`
`επ_num` 📖	CompOp	3 math math: `theorem_6`, `corollary_8`, `corollary_8_apply_theorem_6`
`μ_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
`Eθ_eq_abs` 📖	mathematical	—	`Eθ`	—	`Eθ_nonneg`
`Eθ_nonneg` 📖	mathematical	—	`Eθ`	—	—
`Li_identity` 📖	mathematical	—	`Li`	—	`Li.eq_1` `l0`
`Li_identity'` 📖	mathematical	—	`Li`	—	`Li_identity`
`admissible_bound_le_0826` 📖	mathematical	—	`admissible_bound`	—	`sqrt_exp_le_half`
`admissible_bound_mul` 📖	mathematical	—	`admissible_bound`	—	—
`admissible_bound_pos` 📖	mathematical	—	`admissible_bound`	—	—
`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`	—	`BKLNW.Pre_inputs.epsilon_nonneg` `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_23` `table6_mem` `admissible_bound_le_0826`
`corollary_8` 📖	mathematical	`Eθ.numericalBound`	`Eπ` `επ_num`	—	`find_ereal_bin` `corollary_8_apply_theorem_6`
`corollary_8_apply_theorem_6` 📖	mathematical	`Eθ.numericalBound`	`Eπ` `επ_num`	—	`theorem_6_alt` `ereal_exp_ge_max` `ereal_exp_toReal_le` `theorem_6` `ereal_toReal_sub_mono`
`dawson_antitoneOn` 📖	mathematical	—	`dawson`	—	`remark_after_corollary_11`
`dawson_mono_ge_one` 📖	mathematical	—	`dawson`	—	`dawson_antitoneOn`
`dawson_nonneg` 📖	mathematical	—	`dawson`	—	—
`delta_nonneg` 📖	mathematical	—	`δ`	—	—
`delta_term_bound` 📖	mathematical	—	`δ` `admissible_bound`	—	`logx_over_x_bound` `delta_nonneg`
`ereal_exp_ge_max` 📖	—	—	—	—	—
`ereal_exp_toReal_le` 📖	—	—	—	—	—
`ereal_toReal_coe_log` 📖	—	—	—	—	—
`ereal_toReal_sub_mono` 📖	—	—	—	—	—
`find_ereal_bin` 📖	—	—	—	—	—
`h_monotoneOn` 📖	—	—	—	—	—
`hasDerivAt_Li` 📖	mathematical	—	`Li`	—	—
`hasDerivAt_Li_sub_div_log` 📖	mathematical	—	`Li`	—	—
`he` 📖	mathematical	—	`pi` `Li`	—	`RS_prime.eq_417` `Li_identity` `l1` `l2`
`integral_algebra` 📖	mathematical	—	`admissible_bound`	—	—
`integral_one_div_log_sq` 📖	mathematical	—	`Li`	—	`hasDerivAt_Li_sub_div_log`
`integral_term_bound` 📖	mathematical	`Eθ.classicalBound`	`Eθ` `dawson` `admissible_bound`	—	`Eθ_nonneg` `lemma_12` `m_simplify` `dawson_mono_ge_one` `sqrt_log_minus_ge_one` `dawson_nonneg`
`l0` 📖	—	—	—	—	—
`l1` 📖	—	—	—	—	`l0`
`l2` 📖	—	—	—	—	`l0`
`l3` 📖	—	—	—	—	`l1` `l2`
`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`	—	`l3` `Li_identity'`
`lemma_20_a` 📖	mathematical	—	`Li`	—	`hasDerivAt_Li`
`lemma_20_b` 📖 ⚠️	mathematical	—	`Li`	—	—
`logx_over_x_bound` 📖	mathematical	—	`admissible_bound`	—	`admissible_bound_pos` `ratio_mono`
`m_simplify` 📖	—	—	—	—	—
`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` 📖	—	—	—	—	—
`ratio_eq_g` 📖	mathematical	—	`admissible_bound` `g_bound`	—	—
`ratio_mono` 📖	mathematical	—	`admissible_bound`	—	`lemma_10_substep` `ratio_eq_g`
`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`	—	—
`sqrt_exp_le_half` 📖	—	—	—	—	—
`sqrt_log_minus_ge_one` 📖	—	—	—	—	—
`table6_mem` 📖	mathematical	—	`table6`	—	—
`theorem_3` 📖	mathematical	`Eθ.classicalBound`	`Eπ.classicalBound` `μ_asymp`	—	`theorem_3_easy_preconditions` `admissible_bound_mul` `eq_30` `delta_term_bound` `integral_term_bound`
`theorem_3_easy_preconditions` 📖	—	—	—	—	—
`theorem_6` 📖 ⚠️	mathematical	`Eθ.numericalBound`	`Eπ` `επ_num`	—	—
`theorem_6_1` 📖 ⚠️	mathematical	`Eθ.numericalBound`	`Eπ` `Eθ` `Li`	—	—
`theorem_6_2` 📖 ⚠️	—	—	—	—	—
`theorem_6_3` 📖	mathematical	—	`Li`	—	`integral_one_div_log_sq` `h_monotoneOn`
`theorem_6_alt` 📖	mathematical	`Eθ.numericalBound`	`Eπ` `μ_num_2`	—	`theorem_6`

---

← Back to Index