OAI/NumberTheory/Catalan/Analysis/ManuscriptCaseTwoY13LogPrecisionGroup2.lean
18 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.manuscriptCase2Y13YV7Intervalline 10 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV7_arg_eqline 13 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV7_weight_eqline 17 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV7_exact_intervalline 20 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV7_rounded_endpointsline 35 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV7_enclosureline 44 - def
OAI.InternalCatalan.manuscriptCase2Y13YV9Intervalline 54 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV9_arg_eqline 57 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV9_weight_eqline 61 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV9_exact_intervalline 64 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV9_rounded_endpointsline 79 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV9_enclosureline 88 - def
OAI.InternalCatalan.manuscriptCase2Y13YV11Intervalline 98 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV11_arg_eqline 101 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV11_weight_eqline 105 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV11_exact_intervalline 108 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV11_rounded_endpointsline 123 - theorem
OAI.InternalCatalan.manuscriptCase2Y13YV11_enclosureline 132