Ramanujan

📁 Source: PrimeNumberTheoremAnd/Ramanujan.lean

Statistics

Metric	Count
Definitions `C₁`, `C₂`, `C₃`, `Mₐ`, `a`, `exₐ`, `mₐ`, `xₐ`, `ε`, `ε'`, `εlower`, `εneg`	12
Theorems `Li_eq_sub_add_integral`, `a_mono`, `criterion`, `epsilon_bound`, `ex_pi_gt`, `ex_pi_gt_neg`, `ex_pi_gt_nonneg`, `integrable_theta`, `log_7_IBP`, `log_7_int_bound`, `log_8_bound`, `pi_bound`, `pi_bound_1`, `pi_bound_2`, `pi_bound_3`, `pi_bound_4`, `pi_bound_5`, `pi_bound_6`, `pi_error_identity`, `pi_lower`, `pi_lower_specific`, `pi_upper`, `pi_upper_specific`, `ramanujan_final`, `sq_pi_lt`	25
Total	37
⚠️ With sorry `epsilon_bound`, `pi_lower_specific`, `pi_upper_specific`	3

Ramanujan

Definitions

Name	Category	Theorems
`C₁` 📖	CompOp	—
`C₂` 📖	CompOp	—
`C₃` 📖	CompOp	—
`Mₐ` 📖	CompOp	2 math math: `pi_upper_specific`, `epsilon_bound`
`a` 📖	CompOp	2 math math: `a_mono`, `pi_bound`
`exₐ` 📖	CompOp	2 math math: `pi_upper_specific`, `epsilon_bound`
`mₐ` 📖	CompOp	2 math math: `pi_lower_specific`, `epsilon_bound`
`xₐ` 📖	CompOp	3 math math: `pi_lower_specific`, `a_mono`, `epsilon_bound`
`ε` 📖	CompOp	2 math math: `sq_pi_lt`, `epsilon_bound`
`ε'` 📖	CompOp	1 math math: `ex_pi_gt_nonneg`
`εlower` 📖	CompOp	2 math math: `ex_pi_gt`, `epsilon_bound`
`εneg` 📖	CompOp	1 math math: `ex_pi_gt_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Li_eq_sub_add_integral` 📖	mathematical	—	`Li`	—	`Li.eq_1`
`a_mono` 📖	mathematical	—	`a` `xₐ`	—	`admissible_bound.mono`
`criterion` 📖	mathematical	`pi` `ε` `εlower`	`pi`	—	`sq_pi_lt` `ex_pi_gt`
`epsilon_bound` 📖 ⚠️	mathematical	`exₐ`	`ε` `Mₐ` `exₐ` `εlower` `mₐ` `xₐ`	—	—
`ex_pi_gt` 📖	mathematical	`pi`	`pi` `εlower`	—	`ex_pi_gt_nonneg` `ex_pi_gt_neg`
`ex_pi_gt_neg` 📖	mathematical	`pi`	`pi` `εneg`	—	—
`ex_pi_gt_nonneg` 📖	mathematical	`pi`	`pi` `ε'`	—	—
`integrable_theta` 📖	—	—	—	—	—
`log_7_IBP` 📖	—	—	—	—	—
`log_7_int_bound` 📖	—	—	—	—	`log_7_IBP` `log_8_bound`
`log_8_bound` 📖	—	—	—	—	—
`pi_bound` 📖	mathematical	—	`Eθ` `a`	—	`pi_bound_1` `pi_bound_2` `Trudgian2016.lemma_1` `pi_bound_4` `pi_bound_5` `pi_bound_6`
`pi_bound_1` 📖	mathematical	—	`Eθ`	—	—
`pi_bound_2` 📖	mathematical	—	`Eθ`	—	`Buthe2.theorem_2b` `PT_theorem_1`
`pi_bound_3` 📖	mathematical	—	`Eθ`	—	`Trudgian2016.theorem_1_theta`
`pi_bound_4` 📖	mathematical	—	`Eθ`	—	`PT.corollary_1`
`pi_bound_5` 📖	mathematical	—	`Eθ`	—	`PT.corollary_1`
`pi_bound_6` 📖	mathematical	—	`Eθ`	—	`PT.corollary_1`
`pi_error_identity` 📖	mathematical	—	`pi` `Li`	—	`Li_eq_sub_add_integral`
`pi_lower` 📖	mathematical	—	`pi`	—	`integrable_theta` `pi_error_identity` `Li_eq_sub_add_integral`
`pi_lower_specific` 📖 ⚠️	mathematical	`xₐ`	`pi` `mₐ` `xₐ`	—	—
`pi_upper` 📖	mathematical	—	`pi`	—	`pi_error_identity` `Li_eq_sub_add_integral` `integrable_theta`
`pi_upper_specific` 📖 ⚠️	mathematical	`exₐ`	`pi` `Mₐ` `exₐ`	—	—
`ramanujan_final` 📖	mathematical	`exₐ`	`pi`	—	`criterion` `pi_lower_specific` `pi_upper_specific` `epsilon_bound`
`sq_pi_lt` 📖	mathematical	`pi`	`pi` `ε`	—	—

---

← Back to Index