Documentation

LeanPool.Zeta32.Arith.Sum.Pieces

The pieces of psiL and phiL (the proof notes, §8.5).

In the variable u = 1/x (for a prime, u = n/p), the relaxed range (1/20, 7/3] of x is the range [3/7, 20) of u, cut at the points m + α (m ∈ ℕ, α ∈ {0, 1/5, 1/4, 1/3, 2/5, 1/2, 3/5, 2/3, 3/4, 4/5}) into 196 half-open pieces [ub i, ub (i+1)). On the piece with ⌊u⌋ = m and {u} in the k-th cell, psiL x = cellA k m + cellB k m · x − 25/(4x) (the ten parametric formulas, proved once for all m). The outer range (7/3, 5] of x is [1/5, 3/7) in u, four pieces on which phiL is linear. The tail x ≤ 1/20 is handled by the global bound psiL x ≤ 33/5 + (121/100) x.

The cells of `[0,1]` and the ten formulas #

def Zeta32.ArithSum.alphaQ :

Breakpoints of the cells of [0, 1] (partition by j/3, j/4, j/5).

Equations

Instances For

def Zeta32.ArithSum.cellA :

ℕ → ℚ → ℚ

Constant coefficient on cell k (with m = ⌊1/x⌋).

Equations

Zeta32.ArithSum.cellA 0 x✝ = (62 * x✝ + 49) / 4
Zeta32.ArithSum.cellA 1 x✝ = (62 * x✝ + 7) / 4
Zeta32.ArithSum.cellA 2 x✝ = (62 * x✝ + 39) / 4
Zeta32.ArithSum.cellA 3 x✝ = (62 * x✝ + 63) / 4
Zeta32.ArithSum.cellA 4 x✝ = (62 * x✝ + 21) / 4
Zeta32.ArithSum.cellA 5 x✝ = (62 * x✝ + 53) / 4
Zeta32.ArithSum.cellA 6 x✝ = (62 * x✝ + 11) / 4
Zeta32.ArithSum.cellA 7 x✝ = (62 * x✝ + 35) / 4
Zeta32.ArithSum.cellA 8 x✝ = (62 * x✝ + 67) / 4
Zeta32.ArithSum.cellA x✝¹ x✝ = (62 * x✝ + 25) / 4

Instances For

def Zeta32.ArithSum.cellB :

ℕ → ℚ → ℚ

Coefficient of x on cell k.

Equations

Zeta32.ArithSum.cellB 0 x✝ = -(x✝ * (37 * x✝ + 25)) / 4
Zeta32.ArithSum.cellB 1 x✝ = -(37 * x✝ ^ 2 - 5 * x✝ - 6) / 4
Zeta32.ArithSum.cellB 2 x✝ = -(37 * x✝ ^ 2 + 27 * x✝ + 2) / 4
Zeta32.ArithSum.cellB 3 x✝ = -(37 * x✝ ^ 2 + 51 * x✝ + 10) / 4
Zeta32.ArithSum.cellB 4 x✝ = -(37 * x✝ ^ 2 + 21 * x✝ - 2) / 4
Zeta32.ArithSum.cellB 5 x✝ = -(37 * x✝ ^ 2 + 53 * x✝ + 14) / 4
Zeta32.ArithSum.cellB 6 x✝ = -(37 * x✝ ^ 2 + 23 * x✝ - 4) / 4
Zeta32.ArithSum.cellB 7 x✝ = -(37 * x✝ ^ 2 + 47 * x✝ + 12) / 4
Zeta32.ArithSum.cellB 8 x✝ = -(37 * x✝ ^ 2 + 79 * x✝ + 36) / 4
Zeta32.ArithSum.cellB x✝¹ x✝ = -((x✝ + 1) * (37 * x✝ + 12)) / 4

Instances For

theorem Zeta32.ArithSum.fract_eq_sub (y : ℝ) (z : ℤ) (h1 : ↑z ≤ y) (h2 : y < ↑z + 1) :

Int.fract y = y - ↑z

theorem Zeta32.ArithSum.psiL_eq (x : ℝ) :

psiL x = 6 + x * Int.fract (3 / x) * (1 - Int.fract (3 / x)) - 3 * (4 * Int.fract (1 / x) - Int.fract (5 / x)) + x / 4 * (16 * Int.fract (1 / x) + Int.fract (5 / x) - 8 * min (Int.fract (1 / x)) (Int.fract (5 / x)) - (4 * Int.fract (1 / x) - Int.fract (5 / x)) ^ 2)

psiL in terms of the three fractional parts (definitional unfolding).

theorem Zeta32.ArithSum.psiL_cell (k : ℕ) (hk : k < 10) (m : ℕ) {x : ℝ} (hx : 0 < x) (h1 : ↑m + ↑(alphaQ k) ≤ 1 / x) (h2 : 1 / x < ↑m + ↑(alphaQ (k + 1))) :

psiL x = ↑(cellA k ↑m) + ↑(cellB k ↑m) * x - 25 / (4 * x)

The ten parametric formulas: on the cell k of the unit interval, shifted by m.

The 196 pieces of the relaxed range, indexed flatly #

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

Integer part m of piece i (pieces 0..5 have m = 0, cells 4..9).

Equations

Zeta32.ArithSum.pm i = if i < 6 then 0 else (i - 6) / 10 + 1

Instances For

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

Cell k of piece i.

Equations

Zeta32.ArithSum.pk i = if i < 6 then i + 4 else (i - 6) % 10

Instances For

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

Left endpoint (in u = 1/x) of piece i; piece 0 starts at 3/7 inside cell 4.

Equations

Zeta32.ArithSum.ub i = if i = 0 then 3 / 7 else ↑(Zeta32.ArithSum.pm i) + Zeta32.ArithSum.alphaQ (Zeta32.ArithSum.pk i)

Instances For

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

Coefficients of piece i: psiL x = pa i + pb i · x − 25/(4x).

Equations

Zeta32.ArithSum.pa i = Zeta32.ArithSum.cellA (Zeta32.ArithSum.pk i) ↑(Zeta32.ArithSum.pm i)

Instances For

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

Constant term of the affine arithmetic-profile cell selected by i.

Equations

Zeta32.ArithSum.pb i = Zeta32.ArithSum.cellB (Zeta32.ArithSum.pk i) ↑(Zeta32.ArithSum.pm i)

Instances For

theorem Zeta32.ArithSum.pk_lt (i : ℕ) :

pk i < 10

theorem Zeta32.ArithSum.pm_pk_succ (i : ℕ) :

pk i < 9 ∧ pm (i + 1) = pm i ∧ pk (i + 1) = pk i + 1 ∨ pk i = 9 ∧ pm (i + 1) = pm i + 1 ∧ pk (i + 1) = 0

theorem Zeta32.ArithSum.ub_succ (i : ℕ) :

ub (i + 1) = ↑(pm i) + alphaQ (pk i + 1)

theorem Zeta32.ArithSum.ub_ge (i : ℕ) :

↑(pm i) + alphaQ (pk i) ≤ ub i

theorem Zeta32.ArithSum.alphaQ_lt (k : ℕ) (hk : k < 10) :

alphaQ k < alphaQ (k + 1)

theorem Zeta32.ArithSum.ub_lt_succ (i : ℕ) :

ub i < ub (i + 1)

theorem Zeta32.ArithSum.ub_zero :

ub 0 = 3 / 7

theorem Zeta32.ArithSum.ub_196 :

ub 196 = 20

theorem Zeta32.ArithSum.ub_pos (i : ℕ) :

0 < ub i

theorem Zeta32.ArithSum.psiL_piece (i : ℕ) {x : ℝ} (hx : 0 < x) (h1 : ↑(ub i) ≤ 1 / x) (h2 : 1 / x < ↑(ub (i + 1))) :

psiL x = ↑(pa i) + ↑(pb i) * x - 25 / (4 * x)

On piece i (for every i, in particular the 196 pieces of [3/7, 20)), psiL is given by the formula of its cell.

The four pieces of the outer range (`7/3 < x ≤ 5`, i.e. `1/5 ≤ u < 3/7`) #

def Zeta32.ArithSum.vb :

Rational breakpoints for the reciprocal outer-prime profile.

Equations

Instances For

def Zeta32.ArithSum.vc :

Constant terms of the affine pieces of the reciprocal outer-prime profile.

Equations

Instances For

def Zeta32.ArithSum.vd :

Slopes of the affine pieces of the reciprocal outer-prime profile.

Equations

Instances For

theorem Zeta32.ArithSum.vb_lt_succ (i : ℕ) (hi : i < 4) :

vb i < vb (i + 1)

theorem Zeta32.ArithSum.phiL_piece (i : ℕ) (hi : i < 4) {x : ℝ} (hx : 0 < x) (h1 : ↑(vb i) ≤ 1 / x) (h2 : 1 / x < ↑(vb (i + 1))) :

phiL x = ↑(vc i) + ↑(vd i) * x

The tail bound #

theorem Zeta32.ArithSum.quad_bound (a b : ℝ) (j : ℤ) (hj : 5 * a - b = ↑j) (ha0 : 0 ≤ a) (ha1 : a < 1) (hb0 : 0 ≤ b) (hb1 : b < 1) :

16 * a + b - 8 * min a b - (4 * a - b) ^ 2 ≤ 96 / 25 ∧ -3 * (4 * a - b) ≤ 3 / 5

theorem Zeta32.ArithSum.psiL_le_tail {x : ℝ} (hx : 0 < x) :

psiL x ≤ 33 / 5 + 121 / 100 * x

psiL x ≤ 33/5 + (121/100) x for every x > 0 (used for x ≤ 1/20).