Circle integrals of log ‖· - a‖

Consequences of Mathlib's circle-average identities, in the normalisation used here (integrals over θ ∈ [0, 2π] without the factor (2π)⁻¹), and countability of point preimages under circleMap and cos.

theorem Zeta5Irrational.circle_log_integrable (c a : ℂ) (R : ℝ) : IntervalIntegrable (fun (θ : ℝ) => Real.log ‖circleMap c R θ - a‖) MeasureTheory.volume 0 (2 * Real.pi)

theorem Zeta5Irrational.circle_log_integral (c a : ℂ) {R : ℝ} (hR : R ≠ 0) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap c R θ - a‖ = 2 * Real.pi * (Real.log R + (R⁻¹ * ‖c - a‖).posLog)

∫₀^{2π} log ‖circleMap c R θ - a‖ = 2π (log R + log⁺ (R⁻¹ ‖c - a‖)).

theorem Zeta5Irrational.circle_log_integral_zero_one (a : ℂ) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap 0 1 θ - a‖ = 2 * Real.pi * ‖a‖.posLog

theorem Zeta5Irrational.abs_log_eq (x : ℝ) : |Real.log x| = 2 * x.posLog - Real.log x

theorem Zeta5Irrational.posLog_norm_sub_le (w q : ℂ) (hw : ‖w‖ ≤ 1) : ‖w - q‖.posLog ≤ Real.log (1 + ‖q‖)

theorem Zeta5Irrational.abs_log_circle_integral_le (q : ℂ) : ∫ (θ : ℝ) in 0..2 * Real.pi, |Real.log ‖circleMap 0 1 θ - q‖| ≤ 4 * Real.pi * Real.log (1 + ‖q‖)

Uniform bound ∫₀^{2π} |log ‖e^{iθ} - q‖| ≤ 4π log (1 + ‖q‖).

theorem Zeta5Irrational.circleMap_preimage_countable (c : ℂ) {R : ℝ} (hR : R ≠ 0) (z : ℂ) : (circleMap c R ⁻¹' {z}).Countable

Point preimages under circleMap are countable.

theorem Zeta5Irrational.cos_preimage_countable (c : ℝ) : (Real.cos ⁻¹' {c}).Countable

Point preimages under cos are countable.

theorem Zeta5Irrational.circleMap_zero_one_re (θ : ℝ) : (circleMap 0 1 θ).re = Real.cos θ

theorem Zeta5Irrational.cos_eq_half_add_inv (θ : ℝ) : ↑(Real.cos θ) = (circleMap 0 1 θ + (circleMap 0 1 θ)⁻¹) / 2

cos θ = (w + w⁻¹)/2 for w = e^{iθ}.

theorem Zeta5Irrational.norm_circleMap_zero_one (θ : ℝ) : ‖circleMap 0 1 θ‖ = 1