Zeta32 — Arith — Profiles.

noncomputable def Zeta32.ArithSum.psiL (x : ℝ) : ℝ

The fractional-part profile controlling the arithmetic valuation bound.

Equations

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

noncomputable def Zeta32.ArithSum.phiL (x : ℝ) : ℝ

The piecewise affine profile controlling the outer-prime contribution.

Equations

• Zeta32.ArithSum.phiL x = if x ≤ 5 / 2 then 6 - x else if x ≤ 3 then 24 - 7 * x else if x ≤ 4 then 18 - 5 * x else 2 - x