Documentation Verification Report

Li2Bounds

📁 Source: PrimeNumberTheoremAnd/Li2Bounds.lean

Statistics

Metric	Count
Definitions `g`, `li`, `li2_symmetric`	3
Theorems `g_intervalIntegrable`, `g_intervalIntegrable_full`, `integral_sub_left`, `integral_sub_right`, `li2_bounds`, `li2_symmetric_bounds`, `li2_symmetric_eq_Li2_li2`, `li2_symmetric_eq_li2`, `li2_symmetric_lower`, `li2_symmetric_upper`, `li_two_approx_weak_proof`, `limit_integral_g`, `log_one_minus_integrable`, `log_one_plus_integrable`, `pv_integral_eq_symmetric`, `pv_tendsto_li2_symmetric`, `setDiff_decompose`, `setDiff_integral_eq_split`	18
Total	21

Li2Bounds

Definitions

Name	Category	Theorems
`g` 📖	CompOp	4 math math: `g_intervalIntegrable_full`, `limit_integral_g`, `g_intervalIntegrable`, `pv_integral_eq_symmetric`
`li` 📖	CompOp	4 math math: `li_eq_Li2Bounds_li`, `li2_bounds`, `li_two_approx_weak_proof`, `li2_symmetric_eq_li2`
`li2_symmetric` 📖	CompOp	7 math math: `pv_tendsto_li2_symmetric`, `li2_symmetric_lower`, `li2_symmetric_upper`, `li2_symmetric_eq_Li2_li2`, `li2_symmetric_eq_li2`, `li2_symmetric_eq_li2`, `li2_symmetric_bounds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`g_intervalIntegrable` 📖	mathematical	—	`g`	—	`g_intervalIntegrable_full`
`g_intervalIntegrable_full` 📖	mathematical	—	`g`	—	—
`integral_sub_left` 📖	—	—	—	—	—
`integral_sub_right` 📖	—	—	—	—	—
`li2_bounds` 📖	mathematical	—	`li`	—	`li2_symmetric_eq_li2` `li2_symmetric_bounds`
`li2_symmetric_bounds` 📖	mathematical	—	`li2_symmetric`	—	`li2_symmetric_lower` `li2_symmetric_upper`
`li2_symmetric_eq_Li2_li2` 📖	mathematical	—	`li2_symmetric`	—	—
`li2_symmetric_eq_li2` 📖	mathematical	—	`li2_symmetric` `li`	—	`pv_tendsto_li2_symmetric`
`li2_symmetric_lower` 📖	mathematical	—	`li2_symmetric`	—	`li2_symmetric_eq_Li2_li2`
`li2_symmetric_upper` 📖	mathematical	—	`li2_symmetric`	—	`li2_symmetric_eq_Li2_li2`
`li_two_approx_weak_proof` 📖	mathematical	—	`li`	—	`li2_bounds`
`limit_integral_g` 📖	mathematical	—	`g`	—	`g_intervalIntegrable_full`
`log_one_minus_integrable` 📖	—	—	—	—	—
`log_one_plus_integrable` 📖	—	—	—	—	—
`pv_integral_eq_symmetric` 📖	mathematical	—	`g`	—	`integral_sub_left` `integral_sub_right` `log_one_minus_integrable` `log_one_plus_integrable`
`pv_tendsto_li2_symmetric` 📖	mathematical	—	`li2_symmetric`	—	`setDiff_integral_eq_split` `pv_integral_eq_symmetric` `limit_integral_g`
`setDiff_decompose` 📖	—	—	—	—	—
`setDiff_integral_eq_split` 📖	—	—	—	—	`setDiff_decompose`

---

← Back to Index