Documentation

LeanPool.Zeta5Irrational.Table.V08

V08: certified bounds for the zeta(5) proof #

theorem Zeta5Irrational.V_97 :
15510994756587233961 / 312500000000000000000 - 6 * (3 / 40) * -(14366454297200582094051 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2255829004820067 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1109345930554525236403 / 5000000000000000000000) - 6 * (1604875809082805327399 / 5000000000000000000000))) ≤ Vfield (407101159919 / 8000000000000)
theorem Zeta5Irrational.V_98 :
503468730297146605923 / 10000000000000000000000 - 6 * (3 / 40) * -(28601387060477260572887 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1136175792060049 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 89376350887521459017 / 400000000000000000000) - 6 * (318796760635867034687 / 1000000000000000000000))) ≤ Vfield (1652346150993 / 32000000000000)
theorem Zeta5Irrational.V_99 :
510580566961623545383 / 10000000000000000000000 - 6 * (3 / 40) * -(28471572886770229474981 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (457750977922221 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2250001128422295373419 / 10000000000000000000000) - 6 * (1583310802186801713659 / 5000000000000000000000))) ≤ Vfield (167628766231 / 3200000000000)
theorem Zeta5Irrational.V_100 :
6471091867478608207 / 125000000000000000000 - 6 * (3 / 40) * -(28343422312220233724777 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (72032545864051 / 312500000000000 * (Real.pi + (Real.pi / 2 - 2265471525602191722833 / 10000000000000000000000) - 6 * (1572849557147011448877 / 5000000000000000000000))) ≤ Vfield (1700229173627 / 32000000000000)
theorem Zeta5Irrational.V_101 :
524789084785909236581 / 10000000000000000000000 - 6 * (3 / 40) * -(28216893236949584838917 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1160606887629269 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2280822469190898733897 / 10000000000000000000000) - 6 * (3125186301868497031861 / 10000000000000000000000))) ≤ Vfield (107760667809 / 2000000000000)
theorem Zeta5Irrational.V_102 :
134744360763168781831 / 2500000000000000000000 - 6 * (3 / 40) * -(27968538997595321615371 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2353224986307353 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 23111755917091873053 / 100000000000000000000) - 6 * (192833591403646283279 / 625000000000000000000))) ≤ Vfield (886026853789 / 16000000000000)
theorem Zeta5Irrational.V_103 :
138286424721773515033 / 2500000000000000000000 - 6 * (3 / 40) * -(13863101781672242510999 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1192403275103739 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2341078892322328510047 / 10000000000000000000000) - 6 * (3046976284942680492891 / 10000000000000000000000))) ≤ Vfield (454984182553 / 8000000000000)
theorem Zeta5Irrational.V_104 :
72677766318577952713 / 1250000000000000000000 - 6 * (3 / 40) * -(218067756075849292299 / 80000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2446747059541503 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1199801878895283653787 / 5000000000000000000000) - 6 * (594872574128161186261 / 2000000000000000000000))) ≤ Vfield (47892569387 / 800000000000)
theorem Zeta5Irrational.V_105 :
609618831947161312673 / 10000000000000000000000 - 6 * (3 / 40) * -(26811638883410333602363 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1253578883121989 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1228261108513296682027 / 5000000000000000000000) - 6 * (290670848125288106191 / 1000000000000000000000))) ≤ Vfield (502867205187 / 8000000000000)
theorem Zeta5Irrational.V_106 :
63773625144515066253 / 1000000000000000000000 - 6 * (3 / 40) * -(26383922958767512167317 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2566146713712993 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2511944817458580581319 / 10000000000000000000000) - 6 * (2843472865197113350371 / 10000000000000000000000))) ≤ Vfield (65851089563 / 1000000000000)
theorem Zeta5Irrational.V_107 :
161897864139303837243 / 2500000000000000000000 - 6 * (3 / 40) * -(13118980103704165315979 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (646635646287919 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2531071162844353185537 / 10000000000000000000000) - 6 * (2822227043582772569641 / 10000000000000000000000))) ≤ Vfield (2140864814337 / 32000000000000)
theorem Zeta5Irrational.V_108 :
26297478348966672627 / 400000000000000000000 - 6 * (3 / 40) * -(26094097354576342594779 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2606778880784913 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2550029181381709669393 / 10000000000000000000000) - 6 * (1400725358029980269551 / 5000000000000000000000))) ≤ Vfield (1087247381329 / 16000000000000)