LeanPool.Zeta5Irrational.Table.Common

The entries of Table 1 as numerals #

source

theorem Zeta5Irrational.aρ_1 :

aρ 1 = 1953374043 / 500000000000

source

theorem Zeta5Irrational.bρ_1 :

bρ 1 = 8992695531 / 1000000000000

source

theorem Zeta5Irrational.cρ_1 :

cρ 1 = 525779809 / 50000000000

source

theorem Zeta5Irrational.aρ_2 :

aρ 2 = 289031033 / 125000000000

source

theorem Zeta5Irrational.bρ_2 :

bρ 2 = 3068199571 / 200000000000

source

theorem Zeta5Irrational.cρ_2 :

cρ 2 = 29471737793 / 1000000000000

source

theorem Zeta5Irrational.aρ_3 :

aρ 3 = 280457333 / 200000000000

source

theorem Zeta5Irrational.bρ_3 :

bρ 3 = 6432545181 / 250000000000

source

theorem Zeta5Irrational.cρ_3 :

cρ 3 = 42934365099 / 1000000000000

source

theorem Zeta5Irrational.aρ_4 :

aρ 4 = 220431339 / 250000000000

source

theorem Zeta5Irrational.bρ_4 :

bρ 4 = 20954789123 / 500000000000

source

theorem Zeta5Irrational.cρ_4 :

cρ 4 = 29102115983 / 500000000000

source

theorem Zeta5Irrational.aρ_5 :

aρ 5 = 289098953 / 500000000000

source

theorem Zeta5Irrational.bρ_5 :

bρ 5 = 65851089563 / 1000000000000

source

theorem Zeta5Irrational.cρ_5 :

cρ 5 = 6903762131 / 100000000000

source

theorem Zeta5Irrational.aρ_6 :

aρ 6 = 396324613 / 1000000000000

source

theorem Zeta5Irrational.bρ_6 :

bρ 6 = 24870259471 / 250000000000

source

theorem Zeta5Irrational.cρ_6 :

cρ 6 = 78873099189 / 1000000000000

source

theorem Zeta5Irrational.aρ_7 :

aρ 7 = 283911191 / 1000000000000

source

theorem Zeta5Irrational.bρ_7 :

bρ 7 = 72162863729 / 500000000000

source

theorem Zeta5Irrational.cρ_7 :

cρ 7 = 84856120711 / 1000000000000

source

theorem Zeta5Irrational.aρ_8 :

aρ 8 = 53051547 / 250000000000

source

theorem Zeta5Irrational.bρ_8 :

bρ 8 = 201105762729 / 1000000000000

source

theorem Zeta5Irrational.cρ_8 :

cρ 8 = 88396082127 / 1000000000000

source

theorem Zeta5Irrational.aρ_9 :

aρ 9 = 82548843 / 500000000000

source

theorem Zeta5Irrational.bρ_9 :

bρ 9 = 269345996903 / 1000000000000

source

theorem Zeta5Irrational.cρ_9 :

cρ 9 = 706427057 / 8000000000

source

theorem Zeta5Irrational.aρ_10 :

aρ 10 = 33336783 / 250000000000

source

theorem Zeta5Irrational.bρ_10 :

bρ 10 = 86772388539 / 250000000000

source

theorem Zeta5Irrational.cρ_10 :

cρ 10 = 17094464251 / 200000000000

source

theorem Zeta5Irrational.aρ_11 :

aρ 11 = 55761057 / 500000000000

source

theorem Zeta5Irrational.bρ_11 :

bρ 11 = 86161340883 / 200000000000

source

theorem Zeta5Irrational.cρ_11 :

cρ 11 = 39449592119 / 500000000000

source

theorem Zeta5Irrational.aρ_12 :

aρ 12 = 19269871 / 200000000000

source

theorem Zeta5Irrational.bρ_12 :

bρ 12 = 515561896511 / 1000000000000

source

theorem Zeta5Irrational.cρ_12 :

cρ 12 = 35176735959 / 500000000000

source

theorem Zeta5Irrational.aρ_13 :

aρ 13 = 85815639 / 1000000000000

source

theorem Zeta5Irrational.bρ_13 :

bρ 13 = 297724389273 / 500000000000

source

theorem Zeta5Irrational.cρ_13 :

cρ 13 = 11767795323 / 200000000000

source

theorem Zeta5Irrational.aρ_14 :

aρ 14 = 78667711 / 1000000000000

source

theorem Zeta5Irrational.bρ_14 :

bρ 14 = 664241383483 / 1000000000000

source

theorem Zeta5Irrational.cρ_14 :

cρ 14 = 22210660553 / 500000000000

source

theorem Zeta5Irrational.aρ_15 :

aρ 15 = 14825913 / 200000000000

source

theorem Zeta5Irrational.bρ_15 :

bρ 15 = 89520072139 / 125000000000

source

theorem Zeta5Irrational.cρ_15 :

cρ 15 = 30462865791 / 1000000000000

source

theorem Zeta5Irrational.aρ_16 :

aρ 16 = 7174131 / 100000000000

source

theorem Zeta5Irrational.bρ_16 :

bρ 16 = 746637295669 / 1000000000000

source

theorem Zeta5Irrational.cρ_16 :

cρ 16 = 5959622577 / 1000000000000

Upper bounds for the constant values `log ((b_j - a_j)/4)` #

source

theorem Zeta5Irrational.Lmid_1 :

Real.log ((bρ 1 - aρ 1) / 4) ≤ -(66675683038238292067283 / 10000000000000000000000)

source

theorem Zeta5Irrational.Lmid_2 :

Real.log ((bρ 2 - aρ 2) / 4) ≤ -(57268912150832389796717 / 10000000000000000000000)

source

theorem Zeta5Irrational.Lmid_3 :

Real.log ((bρ 3 - aρ 3) / 4) ≤ -(25512130211755314637529 / 5000000000000000000000)

source

theorem Zeta5Irrational.Lmid_4 :

Real.log ((bρ 4 - aρ 4) / 4) ≤ -(11449496158609380585237 / 2500000000000000000000)

source

theorem Zeta5Irrational.Lmid_5 :

Real.log ((bρ 5 - aρ 5) / 4) ≤ -(20577364119368339121527 / 5000000000000000000000)

source

theorem Zeta5Irrational.Lmid_6 :

Real.log ((bρ 6 - aρ 6) / 4) ≤ -(3698074464695343529243 / 1000000000000000000000)

source

theorem Zeta5Irrational.Lmid_7 :

Real.log ((bρ 7 - aρ 7) / 4) ≤ -(33239459906384759787341 / 10000000000000000000000)

source

theorem Zeta5Irrational.Lmid_8 :

Real.log ((bρ 8 - aρ 8) / 4) ≤ -(14956372202312055299661 / 5000000000000000000000)

source

theorem Zeta5Irrational.Lmid_9 :

Real.log ((bρ 9 - aρ 9) / 4) ≤ -(26986659976834617141369 / 10000000000000000000000)

source

theorem Zeta5Irrational.Lmid_10 :

Real.log ((bρ 10 - aρ 10) / 4) ≤ -(12224255358108186379559 / 5000000000000000000000)

source

theorem Zeta5Irrational.Lmid_11 :

Real.log ((bρ 11 - aρ 11) / 4) ≤ -(4457298065613116122159 / 2000000000000000000000)

source

theorem Zeta5Irrational.Lmid_12 :

Real.log ((bρ 12 - aρ 12) / 4) ≤ -(640305991230515290559 / 312500000000000000000)

source

theorem Zeta5Irrational.Lmid_13 :

Real.log ((bρ 13 - aρ 13) / 4) ≤ -(4762195995179309567439 / 2500000000000000000000)

source

theorem Zeta5Irrational.Lmid_14 :

Real.log ((bρ 14 - aρ 14) / 4) ≤ -(8977612329965299982791 / 5000000000000000000000)

source

theorem Zeta5Irrational.Lmid_15 :

Real.log ((bρ 15 - aρ 15) / 4) ≤ -(268788866070650094343 / 156250000000000000000)

source

theorem Zeta5Irrational.Lmid_16 :

Real.log ((bρ 16 - aρ 16) / 4) ≤ -(419641552645073499393 / 250000000000000000000)

source

theorem Zeta5Irrational.Umid_le :

Uρmid ≤ -(28683108419825598767969 / 10000000000000000000000)

Upper bound for the constant value of Uρ on [a₁, b₁].

The entries of Table 1 as numerals #

Upper bounds for the constant values log ((b_j - a_j)/4) #

Upper bounds for the constant values `log ((b_j - a_j)/4)` #