noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highH (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highH x = ⋯ + 1246629436409290235474766554261819684757 / 148728580 * x ^ 69 + 11219664927683612119272898988356377162813 / 452652200 * x ^ 70 + 33658994783050836357818696965069131488439 / 459118660 * x ^ 71 + 11219664927683612119272898988356377162813 / 51731680 * x ^ 72 + 4149739082841883934525592776515372375287 / 6466460 * x ^ 73 + 908792859142372581661104818056866550187853 / 478518040 * x ^ 74 + 908792859142372581661104818056866550187853 / 161661500 * x ^ 75 + 8179135732281353234949943362511798951690677 / 491450960 * x ^ 76 + 24537407196844059704849830087535396855072031 / 497917420 * x ^ 77 + 24537407196844059704849830087535396855072031 / 168127960 * x ^ 78 + 220836664771596537343648470787818571695648279 / 510850340 * x ^ 79 + 662509994314789612030945412363455715086944837 / 517316800 * x ^ 80 + 24537407196844059704849830087535396855072031 / 6466460 * x ^ 81 + 5962589948833106508278508711271101435782503533 / 530249720 * x ^ 82 + 17887769846499319524835526133813304307347510599 / 536716180 * x ^ 83 + 17887769846499319524835526133813304307347510599 / 181060880 * x ^ 84 + 160989928618493875723519735204319738766127595391 / 549649100 * x ^ 85 + 482969785855481627170559205612959216298382786173 / 556115560 * x ^ 86 + 482969785855481627170559205612959216298382786173 / 187527340 * x ^ 87 + 4346728072699334644535032850516632946685445075557 / 569048480 * x ^ 88 + 13040184218098003933605098551549898840056335226671 / 575514940 * x ^ 89 + 4346728072699334644535032850516632946685445075557 / 64664600 * x ^ 90 + 117361657962882035402445886963949089560507017040039 / 588447860 * x ^ 91 + 352084973888646106207337660891847268681521051120117 / 594914320 * x ^ 92 + 352084973888646106207337660891847268681521051120117 / 200460260 * x ^ 93 + 3168764764997814955866038948026625418133689460081053 / 607847240 * x ^ 94 + 9506294294993444867598116844079876254401068380243159 / 614313700 * x ^ 95 + 9506294294993444867598116844079876254401068380243159 / 206926720 * x ^ 96 + 85556648654941003808383051596718886289609615422188431 / 627246620 * x ^ 97 + 1120695014816269453716195119986060190185158159119532153 / 633713080 * x ^ 98 + 3268546859565152161616769197109026164244918960001111 / 71131060 * x ^ 99 + 376259121492074589127334756720578216873389249537685617 / 646646000 * x ^ 100 + 17887990238649770150659457767001538927744346373528031 / 653112460 * x ^ 101 + 15097932299082573260679171089345688203099926779411831 / 43971928 * x ^ 102 + 12873328916171398391755811583716102124042663729815103 / 666045380 * x ^ 103 + 162052139441577972645416858350563096560175035882726289 / 672511840 * x ^ 104 + 479093915376975740542310123657317637322486713052147 / 32332300 * x ^ 105 + 18026528870955423606008504846184168756796496494500543 / 97920680 * x ^ 106 + 1180092601553223330818618710231881904083613186381209 / 98844460 * x ^ 107 + 546717873886599822852403505175309404117192861427141 / 3695120 * x ^ 108 + 91158508521843097327516203771198841088148370723131 / 9153820 * x ^ 109 + 1136637432510031232333243881239574077027011858276253 / 9237800 * x ^ 110 + 2065987528238474320620326805969456651933871351341 / 239020 * x ^ 111 + 76138014883779731575629292582123613451575958569193 / 723520 * x ^ 112 + 1291625144550596298770390238795322448870713913163 / 145996 * x ^ 113 + 4676573799234917633478999140465822659704308995935 / 49096 * x ^ 114 + 171792506910670443678820376588540424234035840667 / 8740 * x ^ 115 + 1049843097787430489148346745818858148096885692965 / 8816 * x ^ 116 + 6362685441135942358474828762538534230890216321 / 52 * x ^ 117 + 1546132562196033993109383389296863818106322566003 / 944 * x ^ 118

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highScalarU : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highScalarU = 392796161 / 100000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highH_deriv (x : ℝ) : HasDerivAt highH (highL x * highG x) x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highH_endpoint : 8 * (highH (7 / 27) - highH 0) ≤ highScalarU

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.highH_rounding : highScalarU < 8 * (highH (7 / 27) - highH 0) + 1 / 100000000