Documentation

LeanCert.Examples.BKLNW_a2_pow2

BKLNW a₂ Definition and 2^N Certificates #

Defines the BKLNW sum function f matching PNT+'s definition, and provides certified upper bounds for (1+α)·f(2^N) via full expansion with finsum_expand.

The function f is defined as: f(x) = Σ_{k=3}^{⌊log(x)/log(2)⌋} x^(1/k - 1/3)

source
noncomputable def LeanCert.Examples.BKLNW_a2_pow2.f (x : ℝ) :
ℝ
Equations
Instances For
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.floor_log_two_pow (n : ℕ) :
    ⌊Real.log (2 ^ n) / Real.log 2⌋₊ = n
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow29_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 29) ≤ 1.4262 + 1 / 10 ^ 4
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow37_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 37) ≤ 1.2195 + 1 / 10 ^ 4
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow44_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 44) ≤ 1.1210 + 1 / 10 ^ 4
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow51_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 51) ≤ 1.07086 + 1 / 10 ^ 5
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow58_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 58) ≤ 1.04319 + 1 / 10 ^ 5
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow63_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 63) ≤ 1.03252 + 1 / 10 ^ 5

    Large-N 2^M certificates (sorry'd interface) #

    These are verified via reflective interval arithmetic in BKLNW_a2_reflective.lean (see pow145_upper etc.), which uses native_decide with Engine.checkBKLNWAlphaPowUpperBound. Sorry'd here to keep compilation fast (same pattern as the exp bounds in BKLNW_a2_bounds.lean).

    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow145_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 145) ≤ 1.0002420 + 1 / 10 ^ 7
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow217_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 217) ≤ 1.000003748 + 1 / 10 ^ 8
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow289_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 289) ≤ 1.00000007713 + 1 / 10 ^ 9
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow361_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 361) ≤ 1.00000002025 + 1 / 10 ^ 9
    source
    theorem LeanCert.Examples.BKLNW_a2_pow2.pow433_upper :
    (1 + 193571378 / 10 ^ 16) * f (2 ^ 433) ≤ 1.00000001938 + 1 / 10 ^ 9