The potential of the comparison measure ρ (closed form) and the field V

• Uω a b t : the closed form (A.1) of the logarithmic potential of the arcsine measure on [a, b];
• Uρ t = ∑ⱼ cⱼ Uω aⱼ bⱼ t for the sixteen intervals of Table 1;
• monotonicity of Uω (nonincreasing left of [a,b], constant on it, nondecreasing right of it);
• the derivative of V: V'(t) = P(√t)/√t with P(y) = π + arctan(1/y) - 6 arctan(α/y).

noncomputable def Zeta5Irrational.Uω (a b t : ℝ) : ℝ

The closed form (A.1) of the potential of the arcsine measure on [a, b].

Equations

• Zeta5Irrational.Uω a b t = if a ≤ t ∧ t ≤ b then Real.log ((b - a) / 4) else Real.log ((|t - (a + b) / 2| + √((t - a) * (t - b))) / 2)

noncomputable def Zeta5Irrational.Uρ (t : ℝ) : ℝ

The potential of ρ.

Equations

• Zeta5Irrational.Uρ t = ∑ j ∈ Finset.Icc 1 16, Zeta5Irrational.cρ j * Zeta5Irrational.Uω (Zeta5Irrational.aρ j) (Zeta5Irrational.bρ j) t

theorem Zeta5Irrational.Uω_of_mem {a b t : ℝ} (h1 : a ≤ t) (h2 : t ≤ b) : Uω a b t = Real.log ((b - a) / 4)

theorem Zeta5Irrational.Uω_of_ge {a b t : ℝ} (hab : a < b) (h : b ≤ t) : Uω a b t = Real.log ((t - (a + b) / 2 + √((t - a) * (t - b))) / 2)

theorem Zeta5Irrational.Uω_of_le {a b t : ℝ} (hab : a < b) (h : t ≤ a) : Uω a b t = Real.log (((a + b) / 2 - t + √((t - a) * (t - b))) / 2)

theorem Zeta5Irrational.Uω_monotoneOn_Ici {a b : ℝ} (hab : a < b) : MonotoneOn (Uω a b) (Set.Ici b)

Uω a b is nondecreasing on [b, ∞).

theorem Zeta5Irrational.Uω_antitoneOn_Iic {a b : ℝ} (hab : a < b) : AntitoneOn (Uω a b) (Set.Iic a)

Uω a b is nonincreasing on (-∞, a].

The derivative of V

noncomputable def Zeta5Irrational.Pfun (y : ℝ) : ℝ

P(y) = π + arctan (1/y) - 6 arctan (α/y).

Equations

• Zeta5Irrational.Pfun y = Real.pi + Real.arctan (1 / y) - 6 * Real.arctan (3 / 40 / y)

noncomputable def Zeta5Irrational.Φ (y : ℝ) : ℝ

The closed form of V as a function of y = √t: Φ(y) = V(y²).

Equations

• Zeta5Irrational.Φ y = Real.log (1 + y ^ 2) - 6 * (3 / 40) * Real.log (y ^ 2 + (3 / 40) ^ 2) - 2 + 12 * (3 / 40) + 2 * y * Zeta5Irrational.Pfun y

theorem Zeta5Irrational.Vfield_eq_Φ {t : ℝ} (ht : 0 < t) : Vfield t = Φ √t

theorem Zeta5Irrational.hasDerivAt_Φ {y : ℝ} (hy : 0 < y) : HasDerivAt Φ (2 * Pfun y) y

theorem Zeta5Irrational.Uω_antitoneOn_Iic' {a b : ℝ} (hab : a < b) : AntitoneOn (Uω a b) (Set.Iic b)

Uω a b is nonincreasing on (-∞, b] (constant on [a, b]).

theorem Zeta5Irrational.Uω_monotoneOn_Ici' {a b : ℝ} (hab : a < b) : MonotoneOn (Uω a b) (Set.Ici a)

Uω a b is nondecreasing on [a, ∞) (constant on [a, b]).

Facts about Table 1

theorem Zeta5Irrational.aρ_lt_bρ (j : ℕ) : j ∈ Finset.Icc 1 16 → aρ j < bρ j

theorem Zeta5Irrational.cρ_pos (j : ℕ) : j ∈ Finset.Icc 1 16 → 0 < cρ j

theorem Zeta5Irrational.aρ_one_le_bρ (j : ℕ) : j ∈ Finset.Icc 1 16 → aρ 1 ≤ bρ j

theorem Zeta5Irrational.aρ_le_bρ_one (j : ℕ) : j ∈ Finset.Icc 1 16 → aρ j ≤ bρ 1

theorem Zeta5Irrational.aρ_le_aρ_one (j : ℕ) : j ∈ Finset.Icc 1 16 → aρ j ≤ aρ 1

theorem Zeta5Irrational.bρ_one_le_bρ (j : ℕ) : j ∈ Finset.Icc 1 16 → bρ 1 ≤ bρ j

theorem Zeta5Irrational.Uρ_antitoneOn : AntitoneOn Uρ (Set.Iic (aρ 1))

Uρ is nonincreasing on (-∞, a₁].

theorem Zeta5Irrational.Uρ_monotoneOn : MonotoneOn Uρ (Set.Ici (bρ 1))

Uρ is nondecreasing on [b₁, ∞).

theorem Zeta5Irrational.Uρ_of_mem {t : ℝ} (h1 : aρ 1 ≤ t) (h2 : t ≤ bρ 1) : Uρ t = ∑ j ∈ Finset.Icc 1 16, cρ j * Real.log ((bρ j - aρ j) / 4)

Uρ is constant on [a₁, b₁].

Monotonicity of P and unimodality of Φ

theorem Zeta5Irrational.hasDerivAt_Pfun {y : ℝ} (hy : 0 < y) : HasDerivAt Pfun (-1 / (y ^ 2 + 1) + 6 * (3 / 40) / (y ^ 2 + (3 / 40) ^ 2)) y

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.y0 : ℝ

The turning point y₀² = 711/880 of P.

Equations

• Zeta5Irrational.y0 = √(711 / 880)

theorem Zeta5Irrational.deriv_Pfun_nonneg {y : ℝ} (hy : 0 < y) (hy0 : y ≤ y0) : 0 ≤ -1 / (y ^ 2 + 1) + 6 * (3 / 40) / (y ^ 2 + (3 / 40) ^ 2)

theorem Zeta5Irrational.deriv_Pfun_nonpos {y : ℝ} (hy0 : y0 ≤ y) : -1 / (y ^ 2 + 1) + 6 * (3 / 40) / (y ^ 2 + (3 / 40) ^ 2) ≤ 0

theorem Zeta5Irrational.Pfun_monotoneOn : MonotoneOn Pfun (Set.Ioc 0 y0)

theorem Zeta5Irrational.Pfun_antitoneOn : AntitoneOn Pfun (Set.Ici y0)

theorem Zeta5Irrational.arctan_le_self' {x : ℝ} (hx : 0 ≤ x) : Real.arctan x ≤ x

theorem Zeta5Irrational.Pfun_pos_of_one_le {y : ℝ} (hy : 1 ≤ y) : 0 < Pfun y

theorem Zeta5Irrational.Pfun_one_pos : 0 < Pfun 1

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.qm : ℝ

The bracket [q₋, q₊] of the paper (Appendix A.3).

Equations

• Zeta5Irrational.qm = 59205077 / 10 ^ 10

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.qp : ℝ

Upper rational endpoint of the bracket around the minimum of the external field.

Equations

• Zeta5Irrational.qp = 59205079 / 10 ^ 10

theorem Zeta5Irrational.sqrt_qm_le_y0 : √qm ≤ y0

theorem Zeta5Irrational.sqrt_qp_le_y0 : √qp ≤ y0

theorem Zeta5Irrational.sqrt_qm_pos : 0 < √qm

theorem Zeta5Irrational.sqrt_qp_pos : 0 < √qp

theorem Zeta5Irrational.Pfun_sqrt_qm_neg : Pfun √qm < 0

Numerical fact: P(√q₋) < 0 (certified).

theorem Zeta5Irrational.Pfun_sqrt_qp_pos : 0 < Pfun √qp

Numerical fact: 0 < P(√q₊) (certified).

theorem Zeta5Irrational.Pfun_nonpos {y : ℝ} (hy : 0 < y) (hy' : y ≤ √qm) : Pfun y ≤ 0

P ≤ 0 on (0, √q₋].

theorem Zeta5Irrational.Pfun_nonneg {y : ℝ} (hy : √qp ≤ y) : 0 ≤ Pfun y

0 ≤ P on [√q₊, ∞).

theorem Zeta5Irrational.Φ_antitoneOn : AntitoneOn Φ (Set.Ioc 0 √qm)

Φ is nonincreasing on (0, √q₋].

theorem Zeta5Irrational.Φ_monotoneOn : MonotoneOn Φ (Set.Ici √qp)

Φ is nondecreasing on [√q₊, ∞).

theorem Zeta5Irrational.Vfield_antitoneOn : AntitoneOn Vfield (Set.Ioc 0 qm)

V is nonincreasing on (0, q₋].

theorem Zeta5Irrational.Vfield_monotoneOn : MonotoneOn Vfield (Set.Ici qp)

V is nondecreasing on [q₊, ∞).