SecondaryDefinitions
📁 Source: PrimeNumberTheoremAnd/SecondaryDefinitions.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 9 | |
| Total | 9 |
⚠️ With sorrytwo_approx | 1 |
(root)
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
li2_symmetric_eq_li2 📖 | mathematical | — | Li2Bounds.li2_symmetricli | — | li_eq_Li2Bounds_liLi2Bounds.li2_symmetric_eq_li2 |
li_eq_Li2Bounds_li 📖 | mathematical | — | liLi2Bounds.li | — | — |
log_ge 📖 | — | — | — | — | — |
log_ge' 📖 | — | — | — | — | — |
log_le 📖 | — | — | — | — | — |
symm_inv_log 📖 | — | — | — | — | log_ge'log_lelog_ge |
li
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
sub_Li 📖 | mathematical | — | liLi | — | Li2Bounds.setDiff_integral_eq_splitLi2Bounds.pv_tendsto_li2_symmetricLi2Bounds.li2_symmetric_eq_li2 |
two_approx 📖 ⚠️ | mathematical | — | li | — | — |
two_approx_weak 📖 | mathematical | — | li | — | li_eq_Li2Bounds_liLi2Bounds.li_two_approx_weak_proof |
---