OAI/NumberTheory/Catalan/Analysis/ManuscriptCaseTwoX5LogPrecisionGroup0.lean
18 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.manuscriptCase2X5XP0Intervalline 9 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP0_arg_eqline 12 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP0_weight_eqline 16 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP0_exact_intervalline 19 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP0_rounded_endpointsline 34 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP0_enclosureline 43 - def
OAI.InternalCatalan.manuscriptCase2X5XP1Intervalline 53 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP1_arg_eqline 56 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP1_weight_eqline 60 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP1_exact_intervalline 63 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP1_rounded_endpointsline 78 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP1_enclosureline 87 - def
OAI.InternalCatalan.manuscriptCase2X5XP2Intervalline 97 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP2_arg_eqline 100 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP2_weight_eqline 104 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP2_exact_intervalline 107 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP2_rounded_endpointsline 122 - theorem
OAI.InternalCatalan.manuscriptCase2X5XP2_enclosureline 131