OAI/NumberTheory/Catalan/Analysis/CauchyLogJump.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.complex_log_neg_of_im_pos line 10
2. theorem OAI.InternalCatalan.complex_log_neg_of_im_neg line 16
3. def OAI.InternalCatalan.cauchyLogLeft line 22
4. def OAI.InternalCatalan.cauchyLogRight line 26
5. theorem OAI.InternalCatalan.cauchyLogLeft_sub_cauchyLogRight line 30
6. theorem OAI.InternalCatalan.cauchyLogLeft_sub_cauchyLogRight_of_abs_im_lt line 50