Documentation

LeanPool.Zeta32.Arith.Sum.Numerics

The numerical constant of the finite-piece route (the proof notes, §8.5).

midRat = Σ over the 196 relaxed pieces of a_J |J| + b_J (x₂² − x₁²)/2 (exact rational; one kernel decide per block of at most 10 pieces, about 200 rational operations each);
log (140/3) > 3842/1000 from log 2 > 0.6931471803 and eight terms of the series of log (1 − 13/48);
tailConst/20 + midRat + 35/36 − (25/4)·(3842/1000) < 283/50.

The rational midRat + tailConst'/20 + 35/36 with the addendum's tail constant is Q_lean of results/lean-route-A.out; here the tail constant is 33/5 + 121/2000 (slightly weaker than 33/5 + 28/500, see psiL_le_tail).

def Zeta32.ArithSum.pieceRat (i : ℕ) :

Exact integral of pa i + pb i · x over piece i in x (from 1/ub (i+1) to 1/ub i).

Equations

One or more equations did not get rendered due to their size.

Instances For

def Zeta32.ArithSum.blockSum (m : ℕ) :

Block m of ten pieces (pieces 6 + 10 m, …, 15 + 10 m, i.e. ⌊1/x⌋ = m + 1).

Equations

Zeta32.ArithSum.blockSum m = ∑ k ∈ Finset.range 10, Zeta32.ArithSum.pieceRat (6 + 10 * m + k)

Instances For

theorem Zeta32.ArithSum.sum_blocks (f : ℕ → ℚ) (M : ℕ) :

∑ i ∈ Finset.range (6 + 10 * M), f i = ∑ i ∈ Finset.range 6, f i + ∑ m ∈ Finset.range M, ∑ k ∈ Finset.range 10, f (6 + 10 * m + k)

theorem Zeta32.ArithSum.block_first :

∑ k ∈ Finset.range 6, pieceRat k = 1009 / 144

theorem Zeta32.ArithSum.block_0 :

blockSum 0 = 4015 / 672

theorem Zeta32.ArithSum.block_1 :

blockSum 1 = 152363 / 51480

theorem Zeta32.ArithSum.block_2 :

blockSum 2 = 616250519 / 310390080

theorem Zeta32.ArithSum.block_3 :

blockSum 3 = 4012219219 / 2677114440

theorem Zeta32.ArithSum.block_4 :

blockSum 4 = 3283464907 / 2724081360

theorem Zeta32.ArithSum.block_5 :

blockSum 5 = 124791792809 / 123712617600

theorem Zeta32.ArithSum.block_6 :

blockSum 6 = 12118655774737 / 13968448253760

theorem Zeta32.ArithSum.block_7 :

blockSum 7 = 328867465879 / 432013982400

theorem Zeta32.ArithSum.block_8 :

blockSum 8 = 27420989731061 / 40430669872320

theorem Zeta32.ArithSum.block_9 :

blockSum 9 = 14470067125139 / 23659965769440

theorem Zeta32.ArithSum.block_10 :

blockSum 10 = 18445124464849 / 33120847987920

theorem Zeta32.ArithSum.block_11 :

blockSum 11 = 141300797426723 / 276398980166400

theorem Zeta32.ArithSum.block_12 :

blockSum 12 = 4153872264547 / 8791663949640

theorem Zeta32.ArithSum.block_13 :

blockSum 13 = 4351654092363449 / 9908021983933920

theorem Zeta32.ArithSum.block_14 :

blockSum 14 = 1036993512889637 / 2527297896689280

theorem Zeta32.ArithSum.block_15 :

blockSum 15 = 100380564220117 / 260728810742400

theorem Zeta32.ArithSum.block_16 :

blockSum 16 = 85354574727978923 / 235376990336648160

theorem Zeta32.ArithSum.block_17 :

blockSum 17 = 1061963532040441 / 3098647368016200

theorem Zeta32.ArithSum.block_18 :

blockSum 18 = 1088835113079157 / 3351473441796480

def Zeta32.ArithSum.midRat :

The rational part of the 196 relaxed pieces.

Equations

Zeta32.ArithSum.midRat = 100640561701307678525350005057360349523 / 3548246127954628149396735699088377600

Instances For

theorem Zeta32.ArithSum.sum_pieceRat :

∑ i ∈ Finset.range 196, pieceRat i = midRat

theorem Zeta32.ArithSum.log_140_div_3_gt :

3842 / 1000 < Real.log (140 / 3)

log (140/3) > 3.842.

def Zeta32.ArithSum.tailConst :

Tail constant: psiL x ≤ tailConst for 0 < x ≤ 1/20.

Equations

Zeta32.ArithSum.tailConst = 33 / 5 + 121 / 2000

Instances For

theorem Zeta32.ArithSum.constant_lt :

↑tailConst / 20 + ↑midRat + 35 / 36 - 25 / 4 * Real.log (140 / 3) < 283 / 50