Poisson-kernel integrals on the unit circle, in the interval-integral form used by the component potentials of the proof notes (8′). PK w θ is the Poisson kernel Re((e^{iθ}+w)/(e^{iθ}−w)). The three facts: ∫₀^{2π} PK w = 2π, ∫₀^{2π} PK w · log|e^{iθ} − q| = 2π log|w − q| for |q| ≥ 1, and ∫₀^{2π} log|e^{iθ} − q| = 2π log⁺|q|; all from Mathlib's Poisson/Jensen formulas.

noncomputable def Zeta32.Analytic.EnergyI.PK (w : ℂ) (θ : ℝ) : ℝ

The Poisson kernel of the unit disc at w, on the unit circle.

Equations

• Zeta32.Analytic.EnergyI.PK w θ = (herglotzRieszKernel 0 w (circleMap 0 1 θ)).re

theorem Zeta32.Analytic.EnergyI.circleAverage_eq_integral (f : ℂ → ℝ) : Real.circleAverage f 0 1 = (2 * Real.pi)⁻¹ * ∫ (θ : ℝ) in 0..2 * Real.pi, f (circleMap 0 1 θ)

theorem Zeta32.Analytic.EnergyI.continuous_PK {w : ℂ} (hw : ‖w‖ < 1) : Continuous (PK w)

theorem Zeta32.Analytic.EnergyI.integral_PK {w : ℂ} (hw : ‖w‖ < 1) : ∫ (θ : ℝ) in 0..2 * Real.pi, PK w θ = 2 * Real.pi

theorem Zeta32.Analytic.EnergyI.integral_PK_log_sphere {w q : ℂ} (hw : ‖w‖ < 1) (hq : ‖q‖ = 1) : ∫ (θ : ℝ) in 0..2 * Real.pi, PK w θ * Real.log ‖circleMap 0 1 θ - q‖ = 2 * Real.pi * Real.log ‖w - q‖

Poisson formula for log|· − q|, |q| = 1.

theorem Zeta32.Analytic.EnergyI.integral_PK_log_out {w q : ℂ} (hw : ‖w‖ < 1) (hq : 1 < ‖q‖) : ∫ (θ : ℝ) in 0..2 * Real.pi, PK w θ * Real.log ‖circleMap 0 1 θ - q‖ = 2 * Real.pi * Real.log ‖w - q‖

Poisson formula for log|· − q|, |q| > 1 (harmonic on a neighbourhood of the closed disc).

theorem Zeta32.Analytic.EnergyI.integral_log_circle (q : ℂ) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap 0 1 θ - q‖ = 2 * Real.pi * ‖q‖.posLog

Jensen: ∫₀^{2π} log|e^{iθ} − q| = 2π log⁺|q|.

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_log_circle (q : ℂ) : IntervalIntegrable (fun (θ : ℝ) => Real.log ‖circleMap 0 1 θ - q‖) MeasureTheory.volume 0 (2 * Real.pi)

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_PK_log_circle {w : ℂ} (hw : ‖w‖ < 1) (q : ℂ) : IntervalIntegrable (fun (θ : ℝ) => PK w θ * Real.log ‖circleMap 0 1 θ - q‖) MeasureTheory.volume 0 (2 * Real.pi)

theorem Zeta32.Analytic.EnergyI.PK_I_mul (β b θ : ℝ) (hβ : β ^ 2 < 1) (hb : b = β ∨ b = -β) : PK (Complex.I * ↑b) θ = (1 - β ^ 2) / (1 - 2 * b * Real.sin θ + β ^ 2)

Explicit form of PK at w = ±iβ.