Documentation

LeanPool.Zeta5Irrational.Table.V19

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

theorem Zeta5Irrational.V_229 :
196312570291665255689 / 1250000000000000000000 - 6 * (3 / 40) * -(8695478910589005680281 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4123762613683913 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1955649145612707344259 / 5000000000000000000000) - 6 * (224882887845839136873 / 1250000000000000000000))) ≤ Vfield (10883467580171 / 64000000000000)
theorem Zeta5Irrational.V_230 :
197260017728728357033 / 1250000000000000000000 - 6 * (3 / 40) * -(17340584442306510414111 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2067252820721749 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 39204764633408501653 / 100000000000000000000) - 6 * (112155517789191659431 / 625000000000000000000))) ≤ Vfield (5470123807721 / 32000000000000)
theorem Zeta5Irrational.V_231 :
792826990337347588387 / 5000000000000000000000 - 6 * (3 / 40) * -(8645231769943453544543 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2072610413478559 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 785924783077314604701 / 2000000000000000000000) - 6 * (447487048230703640181 / 2500000000000000000000))) ≤ Vfield (10997027650713 / 64000000000000)
theorem Zeta5Irrational.V_232 :
796611043778550434037 / 5000000000000000000000 - 6 * (3 / 40) * -(4310148148915218457899 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (259744274098869 / 625000000000000 * (Real.pi + (Real.pi / 2 - 1969370438785238650359 / 5000000000000000000000) - 6 * (892721195245301638437 / 5000000000000000000000))) ≤ Vfield (345431490187 / 2000000000000)
theorem Zeta5Irrational.V_233 :
804170570046356540339 / 5000000000000000000000 - 6 * (3 / 40) * -(17141590695463957545947 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4177201469832627 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3956884238851918576391 / 10000000000000000000000) - 6 * (177653194295087677753 / 1000000000000000000000))) ≤ Vfield (5583683878263 / 32000000000000)
theorem Zeta5Irrational.V_234 :
1623437368556860115687 / 10000000000000000000000 - 6 * (3 / 40) * -(17043559332240260533931 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2099193281346059 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3974908332220430602867 / 10000000000000000000000) - 6 * (1767753594973346520647 / 10000000000000000000000))) ≤ Vfield (2820231956767 / 16000000000000)
theorem Zeta5Irrational.V_235 :
8192554208785925893 / 50000000000000000000 - 6 * (3 / 40) * -(8473239830903755215511 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2109732645385169 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1996407449528079098729 / 5000000000000000000000) - 6 * (879552057096567979033 / 5000000000000000000000))) ≤ Vfield (1139448789761 / 6400000000000)
theorem Zeta5Irrational.V_236 :
25836900440478381773 / 156250000000000000000 - 6 * (3 / 40) * -(2106291672941955151379 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4240439240248289 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4010605638583281302999 / 10000000000000000000000) - 6 * (54705636809765470191 / 312500000000000000000))) ≤ Vfield (1438505996019 / 8000000000000)
theorem Zeta5Irrational.V_237 :
1683595413202401175063 / 10000000000000000000000 - 6 * (3 / 40) * -(8330385197728652168027 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2141039477139623 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4045846230365333599963 / 10000000000000000000000) - 6 * (86694908410619904871 / 500000000000000000000))) ≤ Vfield (2933792027309 / 16000000000000)
theorem Zeta5Irrational.V_238 :
1713539265424779612481 / 10000000000000000000000 - 6 * (3 / 40) * -(2059341758896377698357 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2161658818542197 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2040321455583755349747 / 5000000000000000000000) - 6 * (343536800730602077419 / 2000000000000000000000))) ≤ Vfield (149528603129 / 800000000000)
theorem Zeta5Irrational.V_239 :
871696860918730643327 / 5000000000000000000000 - 6 * (3 / 40) * -(16292095582403450641143 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2182083328585823 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4115007895609233887117 / 10000000000000000000000) - 6 * (1701916397919497671761 / 10000000000000000000000))) ≤ Vfield (3047352097851 / 16000000000000)
theorem Zeta5Irrational.V_240 :
443289828656272310679 / 2500000000000000000000 - 6 * (3 / 40) * -(4028183258387475971649 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4404636855861387 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2074476423521889182987 / 5000000000000000000000) - 6 * (421643805205669706173 / 2500000000000000000000))) ≤ Vfield (1552066066561 / 8000000000000)