/- Copyright (c) 2026 Terence Tao. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Tao -/ import Sendov.LargeDegree.Monotone /-! # The large-degree claim `Sendov.U_le_Ut` removed the degree from the bound; what is left is the single inequality `Ut α < 1` on `0 ≤ α ≤ 17`, and then `R n α < 1` for every `n ≥ 101`. `Ut` is a rational function of `α` times `(α/(3+α)) ^ 48`, so multiplying by `D = 865200 · (3+α) ^ 49 · γ ^ 4`, `γ = 300 + 47α - α²`, which is positive on `[0,17]`, turns the claim into positivity of the single polynomial `F = D (1 - Ut)` of degree `58`. The two closed forms used are `c 101 α = γ / (100 (3+α))`, `T1 101 α = 1600000 (100-2α)² (3+α)³ / (721 γ⁴)`. A Bernstein certificate on `[0,17]` settles it: all 59 coefficients of `F` in the basis `α^m (17-α)^(58-m)` are positive, so no subdivision of the `α`-range is needed. (The informal write-up splits at `α = 16` and estimates the two pieces separately; that is not necessary once the sharp Beta constant is used, which is what leaves the margin — `Ut` peaks at `α = 17` with value `0.9229`.) ## Why the multiplication is distributed by hand `D (1 - Ut)` must not be handed to `field_simp`: it would clear `(3+α) ^ 49` and `γ ⁴` from both sides at once, leaving `ring` a degree-115 identity that it does not close. `D` already *contains* exactly those denominators, so each of the six terms of `Ut` cancels against it separately. Doing that first (`Sendov.Ut_lt_one`, steps `t1`–`t6`, and `h48` for the `48`-th power) keeps every `ring` call at degree at most `62`, which is the same size as the certificate identity itself. `865200` rather than `865200` is used as the multiplier so that each term separately, not merely their sum, comes out with integer coefficients. ## Main statements * `Sendov.Ut_lt_one`: `Ut α < 1` on `0 ≤ α ≤ 17`; * `Sendov.large_degree`: `R n α < 1` for `n ≥ 101`. -/ namespace Sendov variable {α : ℝ} set_option maxHeartbeats 4000000 in -- a degree-58 identity in one variable; `ring` needs more than the default budget /-- The Bernstein certificate: `F` is positive on `[0,17]`. -/ lemma F_pos (hα : 0 ≤ α) (hα' : α ≤ 17) : 0 < 1122702787291394736448332031899900000000 + 19046325083555631071589567727384404000000 * α + 158421799401305511319831453323336122340000 * α ^ 2 + 861086144839783899262522290902928965732400 * α ^ 3 + 3439408019860839882261371580238947745811319 * α ^ 4 + 10763976190978343059270128976319908699279230 * α ^ 5 + 27482264870203746404049226779511973140100922 * α ^ 6 + 58851751350273881387953189525455032864879976 * α ^ 7 + 107855247587877306122230293103712405510570475 * α ^ 8 + 171759728691636266490365540891679381811794330 * α ^ 9 + 240529488382582584529650966973246412375404200 * α ^ 10 + 299026713527922503750214218383542861883052640 * α ^ 11 + 332584383792637363818110693156644176263245770 * α ^ 12 + 333049929303875184857821696251322094451555300 * α ^ 13 + 301880762905153988961008260011013859110924020 * α ^ 14 + 248778383542817950458457719347804130388393200 * α ^ 15 + 187098708657492312991354787006951375606496810 * α ^ 16 + 128821377534531366266108990532541378516293180 * α ^ 17 + 81419630849957631346647265524754482691775400 * α ^ 18 + 47345231058420765609063602657623737762737040 * α ^ 19 + 25377634631717199993415818405387727249820325 * α ^ 20 + 12558381461678887884336588690871882873720170 * α ^ 21 + 5744808624780589326694261819822529221060710 * α ^ 22 + 2431706095253331452737540626239749451182200 * α ^ 23 + 953157993950838580367703259303917955151865 * α ^ 24 + 346144642670223976596034179062502690180750 * α ^ 25 + 116495518414609472010567246197077176778320 * α ^ 26 + 36336281152740288609221052030650841399360 * α ^ 27 + 10502010275079971287850469706276099760700 * α ^ 28 + 2811408048396859598615803016678577566616 * α ^ 29 + 696637045577195749563697260889295071320 * α ^ 30 + 159631247175312590035611267009797954208 * α ^ 31 + 33785522480785269776966858820750983964 * α ^ 32 + 6594450665275339854415586104207300200 * α ^ 33 + 1184779969344702509178802875319571760 * α ^ 34 + 195478905533580848831244517654808400 * α ^ 35 + 29535092351319878473338799170306705 * α ^ 36 + 4072478636506932555839271140088690 * α ^ 37 + 510306927013451786184096375133350 * α ^ 38 + 57808428584128470185954723726040 * α ^ 39 + 5881482509330352987406470588525 * α ^ 40 + 532894392271418064251604942870 * α ^ 41 + 42515012647728027357611076360 * α ^ 42 + 2939585612233076406278632800 * α ^ 43 + 171946491190832176774496730 * α ^ 44 + 8163588014241841361016900 * α ^ 45 + 287999399301298111575540 * α ^ 46 + 5555726484083859953520 * α ^ 47 - 536551383276446293350 * α ^ 48 - 269167118332858968420 * α ^ 49 - 48279425158933803000 * α ^ 50 - 1759012112154436560 * α ^ 51 + 273395914772406495 * α ^ 52 + 6240162359537050 * α ^ 53 - 1129204084343291 * α ^ 54 + 41554143448524 * α ^ 55 - 721404477395 * α ^ 56 + 6229533730 * α ^ 57 - 21627837 * α ^ 58 := by have hu : (0 : ℝ) ≤ 17 - α := by linarith have h0 : (0:ℝ) ≤ 1122702787291394736448332031899900000000 * (17 - α) ^ 58 := mul_nonneg (by norm_num) (pow_nonneg hu 58) have h1 : (0:ℝ) ≤ 388904288083346622931025909215729068000000 * α ^ 1 * (17 - α) ^ 57 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 1)) (pow_nonneg hu 57) have h2 : (0:ℝ) ≤ 66095616740335374779150673987010161532260000 * α ^ 2 * (17 - α) ^ 56 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 2)) (pow_nonneg hu 56) have h3 : (0:ℝ) ≤ 7345821640480281350499142140546658776321841200 * α ^ 3 * (17 - α) ^ 55 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 3)) (pow_nonneg hu 55) have h4 : (0:ℝ) ≤ 600398748030850807066041679815685800572608040199 * α ^ 4 * (17 - α) ^ 54 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 4)) (pow_nonneg hu 54) have h5 : (0:ℝ) ≤ 38479987967757849353019399973163199134827376858856 * α ^ 5 * (17 - α) ^ 53 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 5)) (pow_nonneg hu 53) have h6 : (0:ℝ) ≤ 2013648131786096177205150562840212460891734276215217 * α ^ 6 * (17 - α) ^ 52 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 6)) (pow_nonneg hu 52) have h7 : (0:ℝ) ≤ 88459088337848664272764574750756035751708812314589560 * α ^ 7 * (17 - α) ^ 51 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 7)) (pow_nonneg hu 51) have h8 : (0:ℝ) ≤ 3328752627388631431253304215842302161184427248710824200 * α ^ 8 * (17 - α) ^ 50 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 8)) (pow_nonneg hu 50) have h9 : (0:ℝ) ≤ 108955148579598077254581984889507974501857717600550300000 * α ^ 9 * (17 - α) ^ 49 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 9)) (pow_nonneg hu 49) have h10 : (0:ℝ) ≤ 3139320986827193043298955183356728835782414071606732250000 * α ^ 10 * (17 - α) ^ 48 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 10)) (pow_nonneg hu 48) have h11 : (0:ℝ) ≤ 80389849002074687648105368735226451202772917094058768000000 * α ^ 11 * (17 - α) ^ 47 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 11)) (pow_nonneg hu 47) have h12 : (0:ℝ) ≤ 1843869779817877110104286469976591396926664444962705440000000 * α ^ 12 * (17 - α) ^ 46 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 12)) (pow_nonneg hu 46) have h13 : (0:ℝ) ≤ 38126021284745149595963616317393007484187425284263404800000000 * α ^ 13 * (17 - α) ^ 45 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 13)) (pow_nonneg hu 45) have h14 : (0:ℝ) ≤ 714519722771974812940511821448225512188719319523829280000000000 * α ^ 14 * (17 - α) ^ 44 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 14)) (pow_nonneg hu 44) have h15 : (0:ℝ) ≤ 12192162072496626088921760868440507818256588279501222400000000000 * α ^ 15 * (17 - α) ^ 43 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 15)) (pow_nonneg hu 43) have h16 : (0:ℝ) ≤ 190149195298252798424521646382266997826378949113808102400000000000 * α ^ 16 * (17 - α) ^ 42 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 16)) (pow_nonneg hu 42) have h17 : (0:ℝ) ≤ 2719453325782140875058402865898661993411332371079473152000000000000 * α ^ 17 * (17 - α) ^ 41 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 17)) (pow_nonneg hu 41) have h18 : (0:ℝ) ≤ 35765156781668343145270939254204039481078844597447447040000000000000 * α ^ 18 * (17 - α) ^ 40 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 18)) (pow_nonneg hu 40) have h19 : (0:ℝ) ≤ 433581369383490123337920330591320005197369743601113088000000000000000 * α ^ 19 * (17 - α) ^ 39 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 19)) (pow_nonneg hu 39) have h20 : (0:ℝ) ≤ 4855120840322429070915669670313005676027625016591872000000000000000000 * α ^ 20 * (17 - α) ^ 38 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 20)) (pow_nonneg hu 38) have h21 : (0:ℝ) ≤ 50303800927352895844904371767120477621293024508175810560000000000000000 * α ^ 21 * (17 - α) ^ 37 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 21)) (pow_nonneg hu 37) have h22 : (0:ℝ) ≤ 482953904720497092819809519030958414936076990756461772800000000000000000 * α ^ 22 * (17 - α) ^ 36 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 22)) (pow_nonneg hu 36) have h23 : (0:ℝ) ≤ 4301697515309799266557277840727716853246295229412212736000000000000000000 * α ^ 23 * (17 - α) ^ 35 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 23)) (pow_nonneg hu 35) have h24 : (0:ℝ) ≤ 35582005974740842580199098139010545771216816653126860800000000000000000000 * α ^ 24 * (17 - α) ^ 34 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 24)) (pow_nonneg hu 34) have h25 : (0:ℝ) ≤ 273535549248031302586908863638264651412739231630163968000000000000000000000 * α ^ 25 * (17 - α) ^ 33 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 25)) (pow_nonneg hu 33) have h26 : (0:ℝ) ≤ 1955426273644204648009173651834541693843095232637140992000000000000000000000 * α ^ 26 * (17 - α) ^ 32 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 26)) (pow_nonneg hu 32) have h27 : (0:ℝ) ≤ 13004222926412994888311248631808734105341900865415413760000000000000000000000 * α ^ 27 * (17 - α) ^ 31 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 27)) (pow_nonneg hu 31) have h28 : (0:ℝ) ≤ 80470387643773112884644249468688475191473557588882227200000000000000000000000 * α ^ 28 * (17 - α) ^ 30 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 28)) (pow_nonneg hu 30) have h29 : (0:ℝ) ≤ 463355476918012102672652719197790300193712035699097600000000000000000000000000 * α ^ 29 * (17 - α) ^ 29 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 29)) (pow_nonneg hu 29) have h30 : (0:ℝ) ≤ 2482344082055683113128185595725000998635940934141870080000000000000000000000000 * α ^ 30 * (17 - α) ^ 28 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 30)) (pow_nonneg hu 28) have h31 : (0:ℝ) ≤ 12369353793584370842106405783534323328114720329863004160000000000000000000000000 * α ^ 31 * (17 - α) ^ 27 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 31)) (pow_nonneg hu 27) have h32 : (0:ℝ) ≤ 57300834405504520484711032055319485636127102860053708800000000000000000000000000 * α ^ 32 * (17 - α) ^ 26 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 32)) (pow_nonneg hu 26) have h33 : (0:ℝ) ≤ 246613403330189144932245957910378250136137902552252416000000000000000000000000000 * α ^ 33 * (17 - α) ^ 25 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 33)) (pow_nonneg hu 25) have h34 : (0:ℝ) ≤ 985246695411671462829426238732411673050896371023872000000000000000000000000000000 * α ^ 34 * (17 - α) ^ 24 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 34)) (pow_nonneg hu 24) have h35 : (0:ℝ) ≤ 3649974776445129628396257437653948413551102593597440000000000000000000000000000000 * α ^ 35 * (17 - α) ^ 23 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 35)) (pow_nonneg hu 23) have h36 : (0:ℝ) ≤ 12522828085409243337307923676013931236910302987550720000000000000000000000000000000 * α ^ 36 * (17 - α) ^ 22 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 36)) (pow_nonneg hu 22) have h37 : (0:ℝ) ≤ 39731340789062838384502107867195079108983927708057600000000000000000000000000000000 * α ^ 37 * (17 - α) ^ 21 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 37)) (pow_nonneg hu 21) have h38 : (0:ℝ) ≤ 116365100653574128528674694068315721419971773857792000000000000000000000000000000000 * α ^ 38 * (17 - α) ^ 20 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 38)) (pow_nonneg hu 20) have h39 : (0:ℝ) ≤ 313971050757264181615490913824916376724876505907200000000000000000000000000000000000 * α ^ 39 * (17 - α) ^ 19 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 39)) (pow_nonneg hu 19) have h40 : (0:ℝ) ≤ 778602881203434272472350446775468799876667539456000000000000000000000000000000000000 * α ^ 40 * (17 - α) ^ 18 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 40)) (pow_nonneg hu 18) have h41 : (0:ℝ) ≤ 1769823234178269115425193251412793044953817153536000000000000000000000000000000000000 * α ^ 41 * (17 - α) ^ 17 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 41)) (pow_nonneg hu 17) have h42 : (0:ℝ) ≤ 3676061908648613727975384722760757591726652129280000000000000000000000000000000000000 * α ^ 42 * (17 - α) ^ 16 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 42)) (pow_nonneg hu 16) have h43 : (0:ℝ) ≤ 6952202666310032877475473290777345311129573785600000000000000000000000000000000000000 * α ^ 43 * (17 - α) ^ 15 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 43)) (pow_nonneg hu 15) have h44 : (0:ℝ) ≤ 11922241592723733002313059523572394705939333120000000000000000000000000000000000000000 * α ^ 44 * (17 - α) ^ 14 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 44)) (pow_nonneg hu 14) have h45 : (0:ℝ) ≤ 18450845478651168634684539530259247984017408000000000000000000000000000000000000000000 * α ^ 45 * (17 - α) ^ 13 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 45)) (pow_nonneg hu 13) have h46 : (0:ℝ) ≤ 25626302281194153741004424813630605199042150400000000000000000000000000000000000000000 * α ^ 46 * (17 - α) ^ 12 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 46)) (pow_nonneg hu 12) have h47 : (0:ℝ) ≤ 31735356381499745521943376637135285074788352000000000000000000000000000000000000000000 * α ^ 47 * (17 - α) ^ 11 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 47)) (pow_nonneg hu 11) have h48 : (0:ℝ) ≤ 34773986078859125604170241648646078618789153800477215677912265790935664780750000000000 * α ^ 48 * (17 - α) ^ 10 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 48)) (pow_nonneg hu 10) have h49 : (0:ℝ) ≤ 33406510810664082686608872230111026353099051641531587806834322064288344554180000000000 * α ^ 49 * (17 - α) ^ 9 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 49)) (pow_nonneg hu 9) have h50 : (0:ℝ) ≤ 27820946523539616021999756980494999341031737804699133246948994617042670678045550000000 * α ^ 50 * (17 - α) ^ 8 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 50)) (pow_nonneg hu 8) have h51 : (0:ℝ) ≤ 19791944456596303161181417657916215477628661862047060146272089595047078222827061000000 * α ^ 51 * (17 - α) ^ 7 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 51)) (pow_nonneg hu 7) have h52 : (0:ℝ) ≤ 11779484527176566489160923853925282151874607361320815965499241151163816336970531507500 * α ^ 52 * (17 - α) ^ 6 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 52)) (pow_nonneg hu 6) have h53 : (0:ℝ) ≤ 5685451710206041407628952698706724254113808400301600724661558108213464738446593549500 * α ^ 53 * (17 - α) ^ 5 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 53)) (pow_nonneg hu 5) have h54 : (0:ℝ) ≤ 2124220422337628714954562682925792634155465583908214661397004639843167881489238854787 * α ^ 54 * (17 - α) ^ 4 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 54)) (pow_nonneg hu 4) have h55 : (0:ℝ) ≤ 572909076732572616057605734230328840239193993814061157407956440967916397115623518120 * α ^ 55 * (17 - α) ^ 3 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 55)) (pow_nonneg hu 3) have h56 : (0:ℝ) ≤ 99530623246032452139763064572679576747235355843313027086842616874975359183988464200 * α ^ 56 * (17 - α) ^ 2 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 56)) (pow_nonneg hu 2) have h57 : (0:ℝ) ≤ 8820861539641882551843091227900257872626927159038875775406157756108783934565132000 * α ^ 57 * (17 - α) ^ 1 := mul_nonneg (mul_nonneg (by norm_num) (pow_nonneg hα 57)) (pow_nonneg hu 1) have h58 : (0:ℝ) ≤ 161598081294237579548393327166198311182821276785721838823669379905701080186270000 * α ^ 58 := mul_nonneg (by norm_num) (pow_nonneg hα 58) have hid : (17 : ℝ) ^ 58 * (1122702787291394736448332031899900000000 + 19046325083555631071589567727384404000000 * α + 158421799401305511319831453323336122340000 * α ^ 2 + 861086144839783899262522290902928965732400 * α ^ 3 + 3439408019860839882261371580238947745811319 * α ^ 4 + 10763976190978343059270128976319908699279230 * α ^ 5 + 27482264870203746404049226779511973140100922 * α ^ 6 + 58851751350273881387953189525455032864879976 * α ^ 7 + 107855247587877306122230293103712405510570475 * α ^ 8 + 171759728691636266490365540891679381811794330 * α ^ 9 + 240529488382582584529650966973246412375404200 * α ^ 10 + 299026713527922503750214218383542861883052640 * α ^ 11 + 332584383792637363818110693156644176263245770 * α ^ 12 + 333049929303875184857821696251322094451555300 * α ^ 13 + 301880762905153988961008260011013859110924020 * α ^ 14 + 248778383542817950458457719347804130388393200 * α ^ 15 + 187098708657492312991354787006951375606496810 * α ^ 16 + 128821377534531366266108990532541378516293180 * α ^ 17 + 81419630849957631346647265524754482691775400 * α ^ 18 + 47345231058420765609063602657623737762737040 * α ^ 19 + 25377634631717199993415818405387727249820325 * α ^ 20 + 12558381461678887884336588690871882873720170 * α ^ 21 + 5744808624780589326694261819822529221060710 * α ^ 22 + 2431706095253331452737540626239749451182200 * α ^ 23 + 953157993950838580367703259303917955151865 * α ^ 24 + 346144642670223976596034179062502690180750 * α ^ 25 + 116495518414609472010567246197077176778320 * α ^ 26 + 36336281152740288609221052030650841399360 * α ^ 27 + 10502010275079971287850469706276099760700 * α ^ 28 + 2811408048396859598615803016678577566616 * α ^ 29 + 696637045577195749563697260889295071320 * α ^ 30 + 159631247175312590035611267009797954208 * α ^ 31 + 33785522480785269776966858820750983964 * α ^ 32 + 6594450665275339854415586104207300200 * α ^ 33 + 1184779969344702509178802875319571760 * α ^ 34 + 195478905533580848831244517654808400 * α ^ 35 + 29535092351319878473338799170306705 * α ^ 36 + 4072478636506932555839271140088690 * α ^ 37 + 510306927013451786184096375133350 * α ^ 38 + 57808428584128470185954723726040 * α ^ 39 + 5881482509330352987406470588525 * α ^ 40 + 532894392271418064251604942870 * α ^ 41 + 42515012647728027357611076360 * α ^ 42 + 2939585612233076406278632800 * α ^ 43 + 171946491190832176774496730 * α ^ 44 + 8163588014241841361016900 * α ^ 45 + 287999399301298111575540 * α ^ 46 + 5555726484083859953520 * α ^ 47 - 536551383276446293350 * α ^ 48 - 269167118332858968420 * α ^ 49 - 48279425158933803000 * α ^ 50 - 1759012112154436560 * α ^ 51 + 273395914772406495 * α ^ 52 + 6240162359537050 * α ^ 53 - 1129204084343291 * α ^ 54 + 41554143448524 * α ^ 55 - 721404477395 * α ^ 56 + 6229533730 * α ^ 57 - 21627837 * α ^ 58) = 1122702787291394736448332031899900000000 * (17 - α) ^ 58 + 388904288083346622931025909215729068000000 * α ^ 1 * (17 - α) ^ 57 + 66095616740335374779150673987010161532260000 * α ^ 2 * (17 - α) ^ 56 + 7345821640480281350499142140546658776321841200 * α ^ 3 * (17 - α) ^ 55 + 600398748030850807066041679815685800572608040199 * α ^ 4 * (17 - α) ^ 54 + 38479987967757849353019399973163199134827376858856 * α ^ 5 * (17 - α) ^ 53 + 2013648131786096177205150562840212460891734276215217 * α ^ 6 * (17 - α) ^ 52 + 88459088337848664272764574750756035751708812314589560 * α ^ 7 * (17 - α) ^ 51 + 3328752627388631431253304215842302161184427248710824200 * α ^ 8 * (17 - α) ^ 50 + 108955148579598077254581984889507974501857717600550300000 * α ^ 9 * (17 - α) ^ 49 + 3139320986827193043298955183356728835782414071606732250000 * α ^ 10 * (17 - α) ^ 48 + 80389849002074687648105368735226451202772917094058768000000 * α ^ 11 * (17 - α) ^ 47 + 1843869779817877110104286469976591396926664444962705440000000 * α ^ 12 * (17 - α) ^ 46 + 38126021284745149595963616317393007484187425284263404800000000 * α ^ 13 * (17 - α) ^ 45 + 714519722771974812940511821448225512188719319523829280000000000 * α ^ 14 * (17 - α) ^ 44 + 12192162072496626088921760868440507818256588279501222400000000000 * α ^ 15 * (17 - α) ^ 43 + 190149195298252798424521646382266997826378949113808102400000000000 * α ^ 16 * (17 - α) ^ 42 + 2719453325782140875058402865898661993411332371079473152000000000000 * α ^ 17 * (17 - α) ^ 41 + 35765156781668343145270939254204039481078844597447447040000000000000 * α ^ 18 * (17 - α) ^ 40 + 433581369383490123337920330591320005197369743601113088000000000000000 * α ^ 19 * (17 - α) ^ 39 + 4855120840322429070915669670313005676027625016591872000000000000000000 * α ^ 20 * (17 - α) ^ 38 + 50303800927352895844904371767120477621293024508175810560000000000000000 * α ^ 21 * (17 - α) ^ 37 + 482953904720497092819809519030958414936076990756461772800000000000000000 * α ^ 22 * (17 - α) ^ 36 + 4301697515309799266557277840727716853246295229412212736000000000000000000 * α ^ 23 * (17 - α) ^ 35 + 35582005974740842580199098139010545771216816653126860800000000000000000000 * α ^ 24 * (17 - α) ^ 34 + 273535549248031302586908863638264651412739231630163968000000000000000000000 * α ^ 25 * (17 - α) ^ 33 + 1955426273644204648009173651834541693843095232637140992000000000000000000000 * α ^ 26 * (17 - α) ^ 32 + 13004222926412994888311248631808734105341900865415413760000000000000000000000 * α ^ 27 * (17 - α) ^ 31 + 80470387643773112884644249468688475191473557588882227200000000000000000000000 * α ^ 28 * (17 - α) ^ 30 + 463355476918012102672652719197790300193712035699097600000000000000000000000000 * α ^ 29 * (17 - α) ^ 29 + 2482344082055683113128185595725000998635940934141870080000000000000000000000000 * α ^ 30 * (17 - α) ^ 28 + 12369353793584370842106405783534323328114720329863004160000000000000000000000000 * α ^ 31 * (17 - α) ^ 27 + 57300834405504520484711032055319485636127102860053708800000000000000000000000000 * α ^ 32 * (17 - α) ^ 26 + 246613403330189144932245957910378250136137902552252416000000000000000000000000000 * α ^ 33 * (17 - α) ^ 25 + 985246695411671462829426238732411673050896371023872000000000000000000000000000000 * α ^ 34 * (17 - α) ^ 24 + 3649974776445129628396257437653948413551102593597440000000000000000000000000000000 * α ^ 35 * (17 - α) ^ 23 + 12522828085409243337307923676013931236910302987550720000000000000000000000000000000 * α ^ 36 * (17 - α) ^ 22 + 39731340789062838384502107867195079108983927708057600000000000000000000000000000000 * α ^ 37 * (17 - α) ^ 21 + 116365100653574128528674694068315721419971773857792000000000000000000000000000000000 * α ^ 38 * (17 - α) ^ 20 + 313971050757264181615490913824916376724876505907200000000000000000000000000000000000 * α ^ 39 * (17 - α) ^ 19 + 778602881203434272472350446775468799876667539456000000000000000000000000000000000000 * α ^ 40 * (17 - α) ^ 18 + 1769823234178269115425193251412793044953817153536000000000000000000000000000000000000 * α ^ 41 * (17 - α) ^ 17 + 3676061908648613727975384722760757591726652129280000000000000000000000000000000000000 * α ^ 42 * (17 - α) ^ 16 + 6952202666310032877475473290777345311129573785600000000000000000000000000000000000000 * α ^ 43 * (17 - α) ^ 15 + 11922241592723733002313059523572394705939333120000000000000000000000000000000000000000 * α ^ 44 * (17 - α) ^ 14 + 18450845478651168634684539530259247984017408000000000000000000000000000000000000000000 * α ^ 45 * (17 - α) ^ 13 + 25626302281194153741004424813630605199042150400000000000000000000000000000000000000000 * α ^ 46 * (17 - α) ^ 12 + 31735356381499745521943376637135285074788352000000000000000000000000000000000000000000 * α ^ 47 * (17 - α) ^ 11 + 34773986078859125604170241648646078618789153800477215677912265790935664780750000000000 * α ^ 48 * (17 - α) ^ 10 + 33406510810664082686608872230111026353099051641531587806834322064288344554180000000000 * α ^ 49 * (17 - α) ^ 9 + 27820946523539616021999756980494999341031737804699133246948994617042670678045550000000 * α ^ 50 * (17 - α) ^ 8 + 19791944456596303161181417657916215477628661862047060146272089595047078222827061000000 * α ^ 51 * (17 - α) ^ 7 + 11779484527176566489160923853925282151874607361320815965499241151163816336970531507500 * α ^ 52 * (17 - α) ^ 6 + 5685451710206041407628952698706724254113808400301600724661558108213464738446593549500 * α ^ 53 * (17 - α) ^ 5 + 2124220422337628714954562682925792634155465583908214661397004639843167881489238854787 * α ^ 54 * (17 - α) ^ 4 + 572909076732572616057605734230328840239193993814061157407956440967916397115623518120 * α ^ 55 * (17 - α) ^ 3 + 99530623246032452139763064572679576747235355843313027086842616874975359183988464200 * α ^ 56 * (17 - α) ^ 2 + 8820861539641882551843091227900257872626927159038875775406157756108783934565132000 * α ^ 57 * (17 - α) ^ 1 + 161598081294237579548393327166198311182821276785721838823669379905701080186270000 * α ^ 58 := by ring rcases le_total α (17 / 2) with h | h · have hpos : (0 : ℝ) < 1122702787291394736448332031899900000000 * (17 - α) ^ 58 := mul_pos (by norm_num) (pow_pos (by linarith) 58) linarith · have hpos : (0 : ℝ) < 161598081294237579548393327166198311182821276785721838823669379905701080186270000 * α ^ 58 := mul_pos (by norm_num) (pow_pos (by linarith) 58) linarith set_option maxHeartbeats 4000000 in /-- **The bound in `α` alone is below `1`.** -/ theorem Ut_lt_one (hα : 0 ≤ α) (hα' : α ≤ 17) : Ut α < 1 := by have h3 : (0 : ℝ) < 3 + α := three_add_pos hα have hg : (0 : ℝ) < 300 + 47 * α - α ^ 2 := by nlinarith have hgne : (300 : ℝ) + 47 * α - α ^ 2 ≠ 0 := hg.ne' have hc : c 101 α = (300 + 47 * α - α ^ 2) / (100 * (3 + α)) := by simp only [c, M] norm_num field_simp ring have hT1 : T1 101 α = 1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3 / (721 * (300 + 47 * α - α ^ 2) ^ 4) := by simp only [T1, hc] norm_num field_simp ring -- `(α/(3+α)) ^ 48` cancels against `(3+α) ^ 49` without expanding either have h48 : (α / (3 + α)) ^ 48 * (3 + α) ^ 49 = α ^ 48 * (3 + α) := by rw [div_pow, show (3 + α) ^ 49 = (3 + α) ^ 48 * (3 + α) from by ring, ← mul_assoc, div_mul_cancel₀ _ (pow_ne_zero 48 h3.ne')] -- the six terms of `Ut`, each multiplied by `D` have t1 : (1 / 6 : ℝ) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 144200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4 := by ring have t2 : 1 / (4 * (3 + α)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 216300 * (3 + α) ^ 48 * (300 + 47 * α - α ^ 2) ^ 4 := by field_simp ring have t3 : (1 / 200 : ℝ) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 4326 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4 := by ring have t4 : 1 / (400 * (3 + α)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 2163 * (3 + α) ^ 48 * (300 + 47 * α - α ^ 2) ^ 4 := by field_simp ring have t5 : 101 / 100 * (1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3 / (721 * (300 + 47 * α - α ^ 2) ^ 4)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 1939200000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 52 := by -- cancel the γ⁴ syntactically; `field_simp` leaves a stray γ⁻¹ here have hne : (721 : ℝ) * (300 + 47 * α - α ^ 2) ^ 4 ≠ 0 := mul_ne_zero (by norm_num) (pow_ne_zero 4 hg.ne') rw [show 101 / 100 * (1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3 / (721 * (300 + 47 * α - α ^ 2) ^ 4)) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 1600000 * (100 - 2 * α) ^ 2 * (3 + α) ^ 3 / (721 * (300 + 47 * α - α ^ 2) ^ 4) * (721 * (300 + 47 * α - α ^ 2) ^ 4) * (1212 * (3 + α) ^ 49) from by ring, div_mul_cancel₀ _ hne] ring have t6 : (100 - 2 * α) ^ 2 / 100 * 101 * 99 / (16 * (3 + α)) * (α / (3 + α)) ^ 48 * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = (21627837 / 4) * (100 - 2 * α) ^ 2 * α ^ 48 * (300 + 47 * α - α ^ 2) ^ 4 := by rw [show (100 - 2 * α) ^ 2 / 100 * 101 * 99 / (16 * (3 + α)) * (α / (3 + α)) ^ 48 * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = ((100 - 2 * α) ^ 2 / 100 * 101 * 99 / (16 * (3 + α)) * (865200 * (300 + 47 * α - α ^ 2) ^ 4)) * ((α / (3 + α)) ^ 48 * (3 + α) ^ 49) from by ring, h48] field_simp ring have hD : (0 : ℝ) < 865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4 := by have h49 := pow_pos h3 49 have hg4 := pow_pos hg 4 positivity have hmul : (1 - Ut α) * (865200 * (3 + α) ^ 49 * (300 + 47 * α - α ^ 2) ^ 4) = 1122702787291394736448332031899900000000 + 19046325083555631071589567727384404000000 * α + 158421799401305511319831453323336122340000 * α ^ 2 + 861086144839783899262522290902928965732400 * α ^ 3 + 3439408019860839882261371580238947745811319 * α ^ 4 + 10763976190978343059270128976319908699279230 * α ^ 5 + 27482264870203746404049226779511973140100922 * α ^ 6 + 58851751350273881387953189525455032864879976 * α ^ 7 + 107855247587877306122230293103712405510570475 * α ^ 8 + 171759728691636266490365540891679381811794330 * α ^ 9 + 240529488382582584529650966973246412375404200 * α ^ 10 + 299026713527922503750214218383542861883052640 * α ^ 11 + 332584383792637363818110693156644176263245770 * α ^ 12 + 333049929303875184857821696251322094451555300 * α ^ 13 + 301880762905153988961008260011013859110924020 * α ^ 14 + 248778383542817950458457719347804130388393200 * α ^ 15 + 187098708657492312991354787006951375606496810 * α ^ 16 + 128821377534531366266108990532541378516293180 * α ^ 17 + 81419630849957631346647265524754482691775400 * α ^ 18 + 47345231058420765609063602657623737762737040 * α ^ 19 + 25377634631717199993415818405387727249820325 * α ^ 20 + 12558381461678887884336588690871882873720170 * α ^ 21 + 5744808624780589326694261819822529221060710 * α ^ 22 + 2431706095253331452737540626239749451182200 * α ^ 23 + 953157993950838580367703259303917955151865 * α ^ 24 + 346144642670223976596034179062502690180750 * α ^ 25 + 116495518414609472010567246197077176778320 * α ^ 26 + 36336281152740288609221052030650841399360 * α ^ 27 + 10502010275079971287850469706276099760700 * α ^ 28 + 2811408048396859598615803016678577566616 * α ^ 29 + 696637045577195749563697260889295071320 * α ^ 30 + 159631247175312590035611267009797954208 * α ^ 31 + 33785522480785269776966858820750983964 * α ^ 32 + 6594450665275339854415586104207300200 * α ^ 33 + 1184779969344702509178802875319571760 * α ^ 34 + 195478905533580848831244517654808400 * α ^ 35 + 29535092351319878473338799170306705 * α ^ 36 + 4072478636506932555839271140088690 * α ^ 37 + 510306927013451786184096375133350 * α ^ 38 + 57808428584128470185954723726040 * α ^ 39 + 5881482509330352987406470588525 * α ^ 40 + 532894392271418064251604942870 * α ^ 41 + 42515012647728027357611076360 * α ^ 42 + 2939585612233076406278632800 * α ^ 43 + 171946491190832176774496730 * α ^ 44 + 8163588014241841361016900 * α ^ 45 + 287999399301298111575540 * α ^ 46 + 5555726484083859953520 * α ^ 47 - 536551383276446293350 * α ^ 48 - 269167118332858968420 * α ^ 49 - 48279425158933803000 * α ^ 50 - 1759012112154436560 * α ^ 51 + 273395914772406495 * α ^ 52 + 6240162359537050 * α ^ 53 - 1129204084343291 * α ^ 54 + 41554143448524 * α ^ 55 - 721404477395 * α ^ 56 + 6229533730 * α ^ 57 - 21627837 * α ^ 58 := by rw [Ut, hT1, sub_mul, one_mul, add_mul, add_mul, add_mul, add_mul, add_mul, t1, t2, t3, t4, t5, t6] ring rw [← sub_pos] have hF := F_pos hα hα' nlinarith [hmul, hF, hD] /-- **The large-degree claim.** Every degree `n ≥ 101`. -/ theorem large_degree {n : ℕ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) (hfeas : c n α ^ 2 ≤ A n α) : R n α < 1 := by have hcpos : (0 : ℝ) < c n α := by have := c_ge_of_large hn hα hα' linarith exact lt_of_le_of_lt (le_trans (R_le_U (by omega) hα hfeas hcpos) (U_le_Ut hn hα hα')) (Ut_lt_one hα hα') end Sendov