Documentation

LeanCert.Examples.BKLNW_a2_bounds

BKLNW a₂ Bounds - Lightweight Interface #

This file provides the lightweight interface for BKLNW (1+α)·f(exp b) bounds. It exports sorry'd theorems matching the exact signatures needed by PNT+.

Purpose #

This module is designed to be fast to compile (~seconds) and is what downstream projects like PNT+ should import. The heavy numerical verification that proves the bounds is in BKLNW_a2_reflective.lean, which uses native_decide and is only needed for LeanCert's CI, not for users of the bounds.

Verification Status #

All bounds are marked with sorry in this file. They are fully verified via reflective interval arithmetic in BKLNW_a2_reflective.lean. This separation allows downstream projects to use the bounds without incurring the ~5 minute compilation cost of numerical verification.

Interface #

The bounds are in the form (1+α)·f(exp b) ∈ [lo, lo + 10^(-m)] where:

f is LeanCert.Examples.BKLNW_a2_pow2.f (= PNT+'s BKLNW.f)
α = 193571378/10^16 (the BKLNW Table 8 margin)
b ∈ {20, 25, 30, 35, 40, 43, 100, 150, 200, 250, 300}

Core Definition #

noncomputable def LeanCert.Examples.BKLNW_a2_bounds.bklnwF (x : ℝ) (N : ℕ) :

The BKLNW function with explicit limit parameter: f(x, N) = Σ_{k=3}^{N} x^(1/k - 1/3)

This matches PNT+'s f when N = ⌊log(x)/log(2)⌋.

Equations

LeanCert.Examples.BKLNW_a2_bounds.bklnwF x N = ∑ k ∈ Finset.Icc 3 N, x ^ (1 / ↑k - 1 / 3)

Instances For

Floor Lemmas #

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_20 :

⌊20 / Real.log 2⌋₊ = 28

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_25 :

⌊25 / Real.log 2⌋₊ = 36

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_30 :

⌊30 / Real.log 2⌋₊ = 43

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_35 :

⌊35 / Real.log 2⌋₊ = 50

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_40 :

⌊40 / Real.log 2⌋₊ = 57

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_43 :

⌊43 / Real.log 2⌋₊ = 62

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_100 :

⌊100 / Real.log 2⌋₊ = 144

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_150 :

⌊150 / Real.log 2⌋₊ = 216

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_200 :

⌊200 / Real.log 2⌋₊ = 288

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_250 :

⌊250 / Real.log 2⌋₊ = 360

theorem LeanCert.Examples.BKLNW_a2_bounds.floor_300 :

⌊300 / Real.log 2⌋₊ = 432

Connection to PNT+ f definition #

theorem LeanCert.Examples.BKLNW_a2_bounds.f_eq_bklnwF_exp (b : ℕ) :

BKLNW_a2_pow2.f (Real.exp ↑b) = bklnwF (Real.exp ↑b) ⌊↑b / Real.log 2⌋₊

Certified (1+α)·f(exp b) Bounds #

All bounds are sorry'd here and verified in BKLNW_a2_reflective.lean via the reflective interval arithmetic engine + native_decide.

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_20_exp_lower :

1.4262 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 20)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_20_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 20) ≤ 1.4262 + 1 / 10 ^ 4

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_25_exp_lower :

1.2195 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 25)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_25_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 25) ≤ 1.2195 + 1 / 10 ^ 4

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_30_exp_lower :

1.1210 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 30)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_30_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 30) ≤ 1.1210 + 1 / 10 ^ 4

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_35_exp_lower :

1.07086 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 35)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_35_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 35) ≤ 1.07086 + 1 / 10 ^ 5

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_40_exp_lower :

1.04319 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 40)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_40_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 40) ≤ 1.04319 + 1 / 10 ^ 5

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_43_exp_lower :

1.03252 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 43)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_43_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 43) ≤ 1.03252 + 1 / 10 ^ 5

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_100_exp_lower :

1.0002420 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 100)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_100_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 100) ≤ 1.0002420 + 1 / 10 ^ 7

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_150_exp_lower :

1.000003748 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 150)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_150_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 150) ≤ 1.000003748 + 1 / 10 ^ 8

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_200_exp_lower :

1.00000007713 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 200)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_200_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 200) ≤ 1.00000007713 + 1 / 10 ^ 9

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_250_exp_lower :

1.00000002025 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 250)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_250_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 250) ≤ 1.00000002025 + 1 / 10 ^ 9

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_300_exp_lower :

1.00000001937 ≤ (1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 300)

theorem LeanCert.Examples.BKLNW_a2_bounds.a2_300_exp_upper :

(1 + 193571378 / 10 ^ 16) * BKLNW_a2_pow2.f (Real.exp 300) ≤ 1.00000001937 + 1 / 10 ^ 9