OAI/NumberTheory/Catalan/Analysis/ManuscriptCaseTwoX8LogPrecisionGroup2.lean
18 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.manuscriptCase2X8XV0Intervalline 10 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV0_arg_eqline 13 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV0_weight_eqline 17 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV0_exact_intervalline 20 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV0_rounded_endpointsline 35 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV0_enclosureline 44 - def
OAI.InternalCatalan.manuscriptCase2X8XV1Intervalline 54 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV1_arg_eqline 57 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV1_weight_eqline 61 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV1_exact_intervalline 64 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV1_rounded_endpointsline 79 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV1_enclosureline 88 - def
OAI.InternalCatalan.manuscriptCase2X8XV2Intervalline 98 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV2_arg_eqline 101 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV2_weight_eqline 105 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV2_exact_intervalline 108 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV2_rounded_endpointsline 123 - theorem
OAI.InternalCatalan.manuscriptCase2X8XV2_enclosureline 132