Documentation

LeanPool.KaltonRoberts.LogBounds

Log bounds for Phi endpoint proofs #

Numerical logarithm bounds proved via the atanh series and exact rational estimates.

E₂ log bounds: Phi 4 (4/7) (3009/10000) #

source
theorem KaltonRoberts.log_lower_18937_70000 :
-817111 / 625000 ≤ Real.log (18937 / 70000)
source
theorem KaltonRoberts.log_lower_3009_10000 :
-12009773 / 10000000 ≤ Real.log (3009 / 10000)
source
theorem KaltonRoberts.log_upper_4_7 :
Real.log (4 / 7) ≤ -5596157 / 10000000
source
theorem KaltonRoberts.log_lower_6991_10000 :
-715923 / 2000000 ≤ Real.log (6991 / 10000)
source
theorem KaltonRoberts.log_lower_9027_10000 :
-1023651 / 10000000 ≤ Real.log (9027 / 10000)
source
theorem KaltonRoberts.log_upper_21063_10000 :
Real.log (21063 / 10000) ≤ 7449329 / 10000000
source
theorem KaltonRoberts.log_upper_6991_2500 :
Real.log (6991 / 2500) ≤ 10283329 / 10000000
source
theorem KaltonRoberts.log_lower_4 :
13862943 / 10000000 ≤ Real.log 4

E₃ log bounds: Phi 4 (2/7) (47/625) #

source
theorem KaltonRoberts.log_lower_47_625 :
-25876041 / 10000000 ≤ Real.log (47 / 625)
source
theorem KaltonRoberts.log_lower_921_4375 :
-7791009 / 5000000 ≤ Real.log (921 / 4375)
source
theorem KaltonRoberts.log_upper_2_7 :
Real.log (2 / 7) ≤ -12527629 / 10000000
source
theorem KaltonRoberts.log_lower_94_125 :
-285019 / 1000000 ≤ Real.log (94 / 125)
source
theorem KaltonRoberts.log_lower_578_625 :
-390889 / 5000000 ≤ Real.log (578 / 625)
source
theorem KaltonRoberts.log_upper_658_625 :
Real.log (658 / 625) ≤ 514533 / 10000000
source
theorem KaltonRoberts.log_upper_2312_625 :
Real.log (2312 / 625) ≤ 6540583 / 5000000

E₄ log bounds: Phi 5 (5/11) (329/1250) #

source
theorem KaltonRoberts.log_lower_2631_13750 :
-16536749 / 10000000 ≤ Real.log (2631 / 13750)
source
theorem KaltonRoberts.log_lower_329_1250 :
-13348411 / 10000000 ≤ Real.log (329 / 1250)
source
theorem KaltonRoberts.log_upper_5_11 :
Real.log (5 / 11) ≤ -7884573 / 10000000
source
theorem KaltonRoberts.log_lower_921_1250 :
-763597 / 2500000 ≤ Real.log (921 / 1250)
source
theorem KaltonRoberts.log_lower_987_625 :
4569183 / 10000000 ≤ Real.log (987 / 625)
source
theorem KaltonRoberts.log_upper_3619_1250 :
Real.log (3619 / 1250) ≤ 5315271 / 5000000
source
theorem KaltonRoberts.log_upper_921_250 :
Real.log (921 / 250) ≤ 1629999 / 1250000
source
theorem KaltonRoberts.log_lower_5 :
16094379 / 10000000 ≤ Real.log 5