the proof notes, 5.4 (Lemma 12), the weight W: W = W2 on [0, ∞) (Lean's arctan (1/0) = 0 convention included), W2 0 = 0, and W2′(x) = (2/3)(2·atan x + π/4 − atan(x/5)/2) ≥ 0 for x ≥ 0, which is the addendum's W′ = (2/3)(π − 2 atan(1/x) + atan(5/x)/2) after atan(1/x) = π/2 − atan x. Written from scratch.

noncomputable def Zeta32.Fstar.W2 (x : ℝ) : ℝ

Closed expression for the potential weight on the nonnegative real axis.

Equations

• Zeta32.Fstar.W2 x = 2 / 3 * (2 * x * Real.arctan x - Real.log (1 + x ^ 2) + Real.pi / 4 * x - x / 2 * Real.arctan (x / 5) + 5 / 4 * Real.log (1 + x ^ 2 / 25))

theorem Zeta32.Fstar.Wt_eq_W2 {x : ℝ} (hx : 0 ≤ x) : Wt x = W2 x

theorem Zeta32.Fstar.hasDerivAt_W2 (x : ℝ) : HasDerivAt W2 (2 / 3 * (2 * Real.arctan x + Real.pi / 4 - Real.arctan (x / 5) / 2)) x

theorem Zeta32.Fstar.continuous_W2 : Continuous W2

theorem Zeta32.Fstar.W2_monotoneOn : MonotoneOn W2 (Set.Ici 0)

theorem Zeta32.Fstar.Wt_mono {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) : Wt x ≤ Wt y

theorem Zeta32.Fstar.Wt_zero : Wt 0 = 0

theorem Zeta32.Fstar.Wt_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ Wt x