Ramanujan
📁 Source: PrimeNumberTheoremAnd/Ramanujan.lean
Statistics
| Metric | Count |
|---|---|
| 12 | |
| 18 | |
| Total | 30 |
| 18 |
Ramanujan
Definitions
| Name | Category | Theorems |
|---|---|---|
C₁ 📖 | CompOp | — |
C₂ 📖 | CompOp | — |
C₃ 📖 | CompOp | — |
Mₐ 📖 | CompOp | |
a 📖 | CompOp | |
mₐ 📖 | CompOp | |
x' 📖 | CompOp | — |
xₐ 📖 | CompOp | |
ε 📖 | CompOp | |
ε' 📖 | CompOp | |
εMₐ 📖 | CompOp | |
εmₐ 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
a_mono 📖 ⚠️ | mathematical | — | axₐ | — | — |
criterion 📖 ⚠️ | — | pix' | — | — | — |
epsilon_bound 📖 ⚠️ | mathematical | — | εMₐεmₐ | — | — |
ex_pi_gt 📖 ⚠️ | mathematical | pi | ε' | — | — |
log_7_int_bound 📖 ⚠️ | — | — | — | — | — |
pi_bound 📖 ⚠️ | mathematical | — | Eθa | — | — |
pi_bound_1 📖 ⚠️ | mathematical | — | Eθ | — | — |
pi_bound_2 📖 ⚠️ | mathematical | — | Eθ | — | — |
pi_bound_3 📖 ⚠️ | mathematical | — | Eθ | — | — |
pi_bound_4 📖 ⚠️ | mathematical | — | Eθ | — | — |
pi_bound_5 📖 ⚠️ | mathematical | — | Eθ | — | — |
pi_error_identity 📖 ⚠️ | mathematical | — | pili | — | — |
pi_lower 📖 ⚠️ | mathematical | — | pi | — | — |
pi_lower_specific 📖 ⚠️ | mathematical | xₐ | pimₐ | — | — |
pi_upper 📖 ⚠️ | mathematical | — | pi | — | — |
pi_upper_specific 📖 ⚠️ | mathematical | xₐ | piMₐ | — | — |
ramanujan_final 📖 ⚠️ | mathematical | xₐ | pi | — | — |
sq_pi_lt 📖 ⚠️ | mathematical | pi | ε | — | — |
---