OAI/NumberTheory/Catalan/Analysis/ManuscriptCaseTwoY4LogPrecisionGroup2.lean
18 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.manuscriptCase2Y4YV7Intervalline 10 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV7_arg_eqline 13 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV7_weight_eqline 17 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV7_exact_intervalline 20 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV7_rounded_endpointsline 35 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV7_enclosureline 44 - def
OAI.InternalCatalan.manuscriptCase2Y4YV9Intervalline 54 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV9_arg_eqline 57 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV9_weight_eqline 61 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV9_exact_intervalline 64 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV9_rounded_endpointsline 79 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV9_enclosureline 88 - def
OAI.InternalCatalan.manuscriptCase2Y4YV11Intervalline 98 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV11_arg_eqline 101 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV11_weight_eqline 105 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV11_exact_intervalline 108 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV11_rounded_endpointsline 123 - theorem
OAI.InternalCatalan.manuscriptCase2Y4YV11_enclosureline 132