EulerMascheroniBounds
📁 Source: PrimeNumberTheoremAnd/EulerMascheroniBounds.lean
Statistics
| Metric | Count |
|---|---|
| 3 | |
| 11 | |
| Total | 14 |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
γ₁ 📖 | CompOp | |
γ₂ 📖 | CompOp | |
γ₃ 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
eulerMascheroniConstant_lb 📖 | mathematical | — | γ₁ | — | eulerMascheroniSeq_diff_lb |
eulerMascheroniSeq_diff_lb 📖 | — | — | — | — | eulerMascheroniSeq_step_lb |
eulerMascheroniSeq_step_lb 📖 | — | — | — | — | — |
euler_maclaurin_decreasing 📖 | mathematical | — | γ₂ | — | — |
euler_maclaurin_tendsto 📖 | mathematical | — | γ₂ | — | — |
hγ_hi 📖 | — | — | — | — | — |
hγ_lo 📖 | — | — | — | — | γ₃_lower_bound |
log_ineq_1 📖 | — | — | — | — | pos_of_mvt |
pos_of_mvt 📖 | — | — | — | — | — |
γ₃_increasing 📖 | mathematical | — | γ₃ | — | — |
γ₃_lower_bound 📖 | mathematical | — | γ₃ | — | γ₃_increasing |
---