Documentation Verification Report

LiSeries

📁 Source: PrimeNumberTheoremAnd/LiSeries.lean

Statistics

Metric	Count
Definitions	0
Theorems `ibp_Ioc_zero_one`, `ibp_Ioi_one`, `integrableOn_exp_neg_div_Ioi_one`, `integrableOn_log_Ioc`, `integrableOn_log_mul_exp_neg_Ioc`, `integrableOn_log_mul_exp_neg_Ioi_one`, `eulerMascheroni_eq_neg_integral`, `eulerMascheroni_eq_split_integral`, `fubini_log_exp_neg`, `hasSum_exp_sub_one`, `hasSum_exp_sub_one_div`, `integral_exp_sub_one_div_eq_tsum`, `integral_log_inv_eq_integral_exp_div`, `li_eq_eulerMascheroni_add_log_log_add_tsum`, `pv_exp_div_eq_gamma_add_log_add_integral`, `li_eq_eulerMascheroni_add_log_log_add_tsum`	16
Total	16

LiSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eulerMascheroni_eq_neg_integral` 📖	—	—	—	—	—
`eulerMascheroni_eq_split_integral` 📖	—	—	—	—	`eulerMascheroni_eq_neg_integral` `fubini_log_exp_neg`
`fubini_log_exp_neg` 📖	—	—	—	—	`FubiniLogExpNeg.integrableOn_log_mul_exp_neg_Ioc` `FubiniLogExpNeg.integrableOn_log_mul_exp_neg_Ioi_one` `FubiniLogExpNeg.ibp_Ioc_zero_one` `FubiniLogExpNeg.ibp_Ioi_one`
`hasSum_exp_sub_one` 📖	—	—	—	—	—
`hasSum_exp_sub_one_div` 📖	—	—	—	—	`hasSum_exp_sub_one`
`integral_exp_sub_one_div_eq_tsum` 📖	—	—	—	—	`hasSum_exp_sub_one_div`
`integral_log_inv_eq_integral_exp_div` 📖	—	—	—	—	—
`li_eq_eulerMascheroni_add_log_log_add_tsum` 📖	mathematical	—	`li`	—	`pv_exp_div_eq_gamma_add_log_add_integral` `integral_exp_sub_one_div_eq_tsum`
`pv_exp_div_eq_gamma_add_log_add_integral` 📖	—	—	—	—	`pv_exp_div_eq_gamma_add_log_add_integral`

LiSeries.FubiniLogExpNeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ibp_Ioc_zero_one` 📖	—	—	—	—	`integrableOn_log_mul_exp_neg_Ioc`
`ibp_Ioi_one` 📖	—	—	—	—	`integrableOn_log_mul_exp_neg_Ioi_one` `integrableOn_exp_neg_div_Ioi_one`
`integrableOn_exp_neg_div_Ioi_one` 📖	—	—	—	—	—
`integrableOn_log_Ioc` 📖	—	—	—	—	—
`integrableOn_log_mul_exp_neg_Ioc` 📖	—	—	—	—	`integrableOn_log_Ioc`
`integrableOn_log_mul_exp_neg_Ioi_one` 📖	—	—	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`li_eq_eulerMascheroni_add_log_log_add_tsum` 📖	mathematical	—	`li`	—	`LiSeries.li_eq_eulerMascheroni_add_log_log_add_tsum`

---

← Back to Index