OAI/NumberTheory/Jacobsthal/Estimates/PVIdentity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.integral_exp_div_neg_eq line 29
2. lemma OAI.Erdos970.integral_exp_div_split line 38
3. lemma OAI.Erdos970.integrableOn_one_sub_exp_neg_div line 47
4. lemma OAI.Erdos970.integrableOn_exp_neg_div_Ioi line 55
5. lemma OAI.Erdos970.integrableOn_exp_sub_one_div line 64
6. lemma OAI.Erdos970.tendsto_integral_one_sub_exp_neg_div line 73
7. lemma OAI.Erdos970.tendsto_integral_exp_neg_div_Ioi line 89
8. lemma OAI.Erdos970.tendsto_integral_exp_sub_one_div line 98
9. lemma OAI.Erdos970.eulerMascheroni_eq_integral line 122
10. lemma OAI.Erdos970.pv_rewrite line 335
11. theorem OAI.Erdos970.pv_exp_div_eq_gamma_add_log_add_integral line 369