The arcsine potential (A.1) and its modulus of continuity

• arc_potential_real : for real t, ∫₀^{2π} log ‖t - y(θ)‖ dθ = 2π Uω a b t;
• Gpot_sub_le : the Hölder-1/2 estimate for log⁺ ‖ζ + s‖ + log⁺ ‖ζ - s‖ used for the circle regularisation error.

noncomputable def Zeta5Irrational.sqR (ζ : ℝ) : ℂ

A square root of ζ² - 1 for real ζ.

Equations

• Zeta5Irrational.sqR ζ = if 1 ≤ ζ ^ 2 then ↑√(ζ ^ 2 - 1) else ↑√(1 - ζ ^ 2) * Complex.I

theorem Zeta5Irrational.sqR_sq (ζ : ℝ) : sqR ζ ^ 2 = ↑ζ ^ 2 - 1

theorem Zeta5Irrational.posLog_sum_real (ζ : ℝ) : ‖↑ζ + sqR ζ‖.posLog + ‖↑ζ - sqR ζ‖.posLog = if 1 ≤ |ζ| then Real.log (|ζ| + √(ζ ^ 2 - 1)) else 0

The value log⁺ ‖ζ + s‖ + log⁺ ‖ζ - s‖ for real ζ.

theorem Zeta5Irrational.Uω_eq_log_add {a b t : ℝ} (hab : a < b) : Uω a b t = Real.log ((b - a) / 4) + if 1 ≤ |(t - (a + b) / 2) / ((b - a) / 2)| then Real.log (|(t - (a + b) / 2) / ((b - a) / 2)| + √(((t - (a + b) / 2) / ((b - a) / 2)) ^ 2 - 1)) else 0

The closed form Uω in terms of ζ = (t - m)/r.

theorem Zeta5Irrational.arc_potential_real {a b : ℝ} (hab : a < b) (t : ℝ) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖↑t - arcCurve ((a + b) / 2) ((b - a) / 2) θ‖ = 2 * Real.pi * Uω a b t

(A.1): the arcsine potential at a real point.

Hölder continuity of the potential

theorem Zeta5Irrational.norm_mul_roots {ζ sq : ℂ} (hsq : sq ^ 2 = ζ ^ 2 - 1) : ‖ζ + sq‖ * ‖ζ - sq‖ = 1

theorem Zeta5Irrational.posLog_sum_eq_log_max {ζ sq : ℂ} (hsq : sq ^ 2 = ζ ^ 2 - 1) : ‖ζ + sq‖.posLog + ‖ζ - sq‖.posLog = Real.log (max ‖ζ + sq‖ ‖ζ - sq‖)

log⁺ ‖ζ + s‖ + log⁺ ‖ζ - s‖ = log (max ‖ζ + s‖ ‖ζ - s‖).

theorem Zeta5Irrational.one_le_max_roots {ζ sq : ℂ} (hsq : sq ^ 2 = ζ ^ 2 - 1) : 1 ≤ max ‖ζ + sq‖ ‖ζ - sq‖

theorem Zeta5Irrational.log_sub_log_le_of_one_le {M M' : ℝ} (hM : 1 ≤ M) (hM' : 1 ≤ M') : Real.log M - Real.log M' ≤ |M - M'|

theorem Zeta5Irrational.abs_log_max_sub_le {M M' : ℝ} (hM : 1 ≤ M) (hM' : 1 ≤ M') : |Real.log M - Real.log M'| ≤ |M - M'|

theorem Zeta5Irrational.max_roots_sub_le_aux (ζ ζ' s s' : ℂ) : |max ‖ζ + s‖ ‖ζ - s‖ - max ‖ζ' + s'‖ ‖ζ' - s'‖| ≤ ‖ζ - ζ'‖ + ‖s - s'‖

theorem Zeta5Irrational.max_roots_sub_le (ζ ζ' s s' : ℂ) : |max ‖ζ + s‖ ‖ζ - s‖ - max ‖ζ' + s'‖ ‖ζ' - s'‖| ≤ ‖ζ - ζ'‖ + min ‖s - s'‖ ‖s + s'‖

theorem Zeta5Irrational.min_roots_le_sqrt (s s' : ℂ) : min ‖s - s'‖ ‖s + s'‖ ≤ √‖s ^ 2 - s' ^ 2‖

theorem Zeta5Irrational.Gpot_sub_le {ζ ζ' s s' : ℂ} (hs : s ^ 2 = ζ ^ 2 - 1) (hs' : s' ^ 2 = ζ' ^ 2 - 1) : ‖ζ + s‖.posLog + ‖ζ - s‖.posLog - (‖ζ' + s'‖.posLog + ‖ζ' - s'‖.posLog) ≤ ‖ζ - ζ'‖ + √(‖ζ - ζ'‖ * ‖ζ + ζ'‖)

The Hölder-1/2 estimate for G(ζ) = log⁺ ‖ζ + s‖ + log⁺ ‖ζ - s‖.