OAI/NumberTheory/Catalan/Analysis/ManuscriptCaseTwoY7LogPrecisionGroup2.lean
18 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.manuscriptCase2Y7YV7Intervalline 10 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV7_arg_eqline 13 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV7_weight_eqline 17 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV7_exact_intervalline 20 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV7_rounded_endpointsline 35 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV7_enclosureline 44 - def
OAI.InternalCatalan.manuscriptCase2Y7YV9Intervalline 54 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV9_arg_eqline 57 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV9_weight_eqline 61 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV9_exact_intervalline 64 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV9_rounded_endpointsline 79 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV9_enclosureline 88 - def
OAI.InternalCatalan.manuscriptCase2Y7YV11Intervalline 98 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV11_arg_eqline 101 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV11_weight_eqline 105 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV11_exact_intervalline 108 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV11_rounded_endpointsline 123 - theorem
OAI.InternalCatalan.manuscriptCase2Y7YV11_enclosureline 132