The arcsine atoms: factorisation and the potential formula (A.1)

For w = e^{iθ} and y(θ) = m + r cos θ, one has z - y(θ) = -(r/(2w)) (w - q₁)(w - q₂) where q₁ + q₂ = 2ζ, q₁ q₂ = 1, ζ = (z - m)/r. Hence ∫₀^{2π} log ‖z - y(θ)‖ dθ = 2π (log (r/2) + log⁺ ‖q₁‖ + log⁺ ‖q₂‖) by Mathlib's circle-average identity, which gives the closed form Uω of (A.1) for real z.

noncomputable def Zeta5Irrational.arcCurve (m r θ : ℝ) : ℂ

The arcsine curve θ ↦ m + r cos θ (as a complex number).

Equations

• Zeta5Irrational.arcCurve m r θ = ↑(m + r * Real.cos θ)

theorem Zeta5Irrational.continuous_arcCurve (m r : ℝ) : Continuous (arcCurve m r)

theorem Zeta5Irrational.norm_arcCurve_le (m r θ : ℝ) : ‖arcCurve m r θ‖ ≤ |m| + |r|

theorem Zeta5Irrational.sub_arcCurve_eq {z : ℂ} {m r : ℝ} (hr : r ≠ 0) (θ : ℝ) {sq : ℂ} (hsq : sq ^ 2 = ((z - ↑m) / ↑r) ^ 2 - 1) : z - arcCurve m r θ = -(↑r / (2 * circleMap 0 1 θ)) * ((circleMap 0 1 θ - ((z - ↑m) / ↑r + sq)) * (circleMap 0 1 θ - ((z - ↑m) / ↑r - sq)))

The factorisation of z - y(θ).

theorem Zeta5Irrational.norm_sub_arcCurve {z : ℂ} {m r : ℝ} (hr : 0 < r) (θ : ℝ) {sq : ℂ} (hsq : sq ^ 2 = ((z - ↑m) / ↑r) ^ 2 - 1) : ‖z - arcCurve m r θ‖ = r / 2 * (‖circleMap 0 1 θ - ((z - ↑m) / ↑r + sq)‖ * ‖circleMap 0 1 θ - ((z - ↑m) / ↑r - sq)‖)

theorem Zeta5Irrational.arc_exceptional_countable (q₁ q₂ : ℂ) : {θ : ℝ | circleMap 0 1 θ = q₁ ∨ circleMap 0 1 θ = q₂}.Countable

The exceptional set is countable.

theorem Zeta5Irrational.arc_log_ae {z : ℂ} {m r : ℝ} (hr : 0 < r) {sq : ℂ} (hsq : sq ^ 2 = ((z - ↑m) / ↑r) ^ 2 - 1) : ∀ᵐ (θ : ℝ), Real.log ‖z - arcCurve m r θ‖ = Real.log (r / 2) + Real.log ‖circleMap 0 1 θ - ((z - ↑m) / ↑r + sq)‖ + Real.log ‖circleMap 0 1 θ - ((z - ↑m) / ↑r - sq)‖

theorem Zeta5Irrational.arc_log_integrable {z : ℂ} {m r : ℝ} (hr : 0 < r) : IntervalIntegrable (fun (θ : ℝ) => Real.log ‖z - arcCurve m r θ‖) MeasureTheory.volume 0 (2 * Real.pi)

theorem Zeta5Irrational.arc_log_integral {z : ℂ} {m r : ℝ} (hr : 0 < r) {sq : ℂ} (hsq : sq ^ 2 = ((z - ↑m) / ↑r) ^ 2 - 1) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖z - arcCurve m r θ‖ = 2 * Real.pi * (Real.log (r / 2) + ‖(z - ↑m) / ↑r + sq‖.posLog + ‖(z - ↑m) / ↑r - sq‖.posLog)

The arcsine potential at a complex point: ∫₀^{2π} log ‖z - y(θ)‖ dθ.

theorem Zeta5Irrational.arc_abs_log_integral_le {z : ℂ} {m r : ℝ} (hr : 0 < r) {sq : ℂ} (hsq : sq ^ 2 = ((z - ↑m) / ↑r) ^ 2 - 1) : ∫ (θ : ℝ) in 0..2 * Real.pi, |Real.log ‖z - arcCurve m r θ‖| ≤ 2 * Real.pi * |Real.log (r / 2)| + 4 * Real.pi * Real.log (1 + ‖(z - ↑m) / ↑r + sq‖) + 4 * Real.pi * Real.log (1 + ‖(z - ↑m) / ↑r - sq‖)

A uniform bound for ∫₀^{2π} |log ‖z - y(θ)‖| dθ.