theorem
G67CenteredEvaluation.profileLog :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (37 / 16) = 940793288338084475929404069391338247984493331965695853573264586860555170665816185023887149199516026647208228297599076306863460352 /
1122224180079198399262262851702839362634888912580547301853088376546424636991182202874175098377149706887625372638538634098524162075
Inspect dependencies
G67CenteredEvaluation.profileLog · compiled type and proof/definition references.
theorem
G67CenteredEvaluation.seLog :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (G67Centered.center / G67Centered.a) = 1503637201134672504441811573125719027659061553778286995349225028492510253377874091176723034080744844728974042620999205358855803270274343136495619850808020907804676126248567147520 /
1798890621739519249499336917028568685012500234884574023075512010129969438616810986654848205253231212355922219916907723677082504346326797873032077371733968393282367427134451105959
Inspect dependencies
G67CenteredEvaluation.seLog · compiled type and proof/definition references.
theorem
G67CenteredEvaluation.slLog :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (2 * G67Centered.b / G67Centered.center) = 83356136645738483683957662324829097300735797855692054655459782410292528365756330076955015881197917097903244884690814904294432471942016430483160240739555998301433471470035346380693921432620172477936214718922117020692320256 /
251783786628055201850977688406924490094007545231352915240319035097003157486324131670342968812316247299080782716062608572039661683553330777298393040343042620421793417362967547079548010052487525077335233637240357719054656225
Inspect dependencies
G67CenteredEvaluation.slLog · compiled type and proof/definition references.
theorem
G67CenteredEvaluation.twoLog :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logUpper 2 = 19540640549631085013602404472737881376887760341733207659 / 28191185216746554583938082208081250592238687381113020900
Inspect dependencies
G67CenteredEvaluation.twoLog · compiled type and proof/definition references.
theorem
G67CenteredEvaluation.reLog :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower
(G67Centered.center ^ 2 / (G67Centered.a * G67Centered.b)) = 470072801804005766339267814674108696509156840014773205681587650759121572692567183272926239598261819101956028832404286464105832726069806280804764655331140967110172312365289125195437070492555752420274871710306532914826086686130531995677831729870589596442873951184103694575646844015129284135390462293895498474818787062397611072930076933385469415004160 /
392396378168802908175471683606237892849354000634545976037521960864568563078293238914023157034312961923430974174564171718509267785619509269621245557173189933151253224132559165203379407026925619110083339609013852251521221022777983202651509775093482878183947830729976558052390533339359438461868600969963829969125405243479989292946450505349948233380573
Inspect dependencies
G67CenteredEvaluation.reLog · compiled type and proof/definition references.
theorem
G67CenteredEvaluation.rmLog :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower (G67Centered.b / G67Centered.a) = 65950865779868241286341246906292389374730392248406166651554921752248327983608712622624452911395657604020873914345906954334860 /
139200177231575000540913611420539494385060560737387374997917880249188693846020408531067587241017041316034446547352995184835249
Inspect dependencies
G67CenteredEvaluation.rmLog · compiled type and proof/definition references.
theorem
G67CenteredEvaluation.rlLog :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower
(G67Centered.b * G67Centered.c / G67Centered.center ^ 2) = 198421986381793279852924633399705468038447978995047952368550064295017728309027931526905921974445047539344792621983051565871329185783957571634692195138878161622570636738795392011867368321623536139468694380698865300328701814386406145064966733300362575937105394616974163468120949020640929320413437762679967009380876820553724487231754240 /
2287005926298289442376355989876465309076193661008402028729923159484185543665471588821087392016207061999021134914622569474569168126177153058433059704362422210179416902916449639309448854488911463967360678164288250040916403527411286462431645148905095275010682803356007714358731766189393160554161586379051213867136002660592797944058134451
Inspect dependencies
G67CenteredEvaluation.rlLog · compiled type and proof/definition references.