The component ρ_c of the proof notes (8′) in angular coordinates.

With t = a cos θ, ρ_c(t) dt on (-a, a) becomes fC θ dθ on (0, 2π) (each t twice), and 4π fC = (P(iβ) + P(−iβ))/2 − c/u_c with β = a/(u_c + c) and P the Poisson kernel of the unit disc: the balayage of δ_{±ic} onto [-a, a] minus a multiple of the arcsine measure (GLOBAL-INTEGRAL-v1 §5).

noncomputable def Zeta32.Analytic.EnergyI.betaC (a c : ℝ) : ℝ

β = a/(u_c + c): ±iβ are the preimages of ±ic inside the unit disc under `w ↦ (a/2)(w

• 1/w)`.

Equations

• Zeta32.Analytic.EnergyI.betaC a c = a / (Zeta32.Analytic.EnergyI.uC a c + c)

noncomputable def Zeta32.Analytic.EnergyI.fC (a c θ : ℝ) : ℝ

Angular density of ρ_c.

Equations

• Zeta32.Analytic.EnergyI.fC a c θ = c * a ^ 2 * Real.sin θ ^ 2 / (4 * Real.pi * Zeta32.Analytic.EnergyI.uC a c * (a ^ 2 * Real.cos θ ^ 2 + c ^ 2))

theorem Zeta32.Analytic.EnergyI.uC_sq (a c : ℝ) : uC a c ^ 2 = c ^ 2 + a ^ 2

theorem Zeta32.Analytic.EnergyI.uC_pos {a : ℝ} (ha : 0 < a) (c : ℝ) : 0 < uC a c

theorem Zeta32.Analytic.EnergyI.c_lt_uC {a c : ℝ} (ha : 0 < a) (hc : 0 ≤ c) : c < uC a c

theorem Zeta32.Analytic.EnergyI.a_lt_uC {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : a < uC a c

theorem Zeta32.Analytic.EnergyI.betaC_pos {a c : ℝ} (ha : 0 < a) (hc : 0 ≤ c) : 0 < betaC a c

theorem Zeta32.Analytic.EnergyI.betaC_mul {a c : ℝ} (ha : 0 < a) (hc : 0 ≤ c) : betaC a c * (uC a c + c) = a

theorem Zeta32.Analytic.EnergyI.betaC_lt_one {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : betaC a c < 1

theorem Zeta32.Analytic.EnergyI.one_sub_betaC_sq {a c : ℝ} (ha : 0 < a) (hc : 0 ≤ c) : 1 - betaC a c ^ 2 = 2 * c / (uC a c + c)

theorem Zeta32.Analytic.EnergyI.one_add_betaC_sq {a c : ℝ} (ha : 0 < a) (hc : 0 ≤ c) : 1 + betaC a c ^ 2 = 2 * uC a c / (uC a c + c)

theorem Zeta32.Analytic.EnergyI.continuous_fC {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : Continuous (fC a c)

theorem Zeta32.Analytic.EnergyI.fC_eq_PK {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (θ : ℝ) : 4 * Real.pi * fC a c θ = (PK (Complex.I * ↑(betaC a c)) θ + PK (Complex.I * ↑(-betaC a c)) θ) / 2 - c / uC a c

The Poisson-kernel form of the angular density.

theorem Zeta32.Analytic.EnergyI.sin_mul_rhoC {a c : ℝ} (ha : 0 < a) (hc : 0 < c) {θ : ℝ} (hθ : θ ∈ Set.Icc 0 Real.pi) : |(-(a * Real.sin θ))| * rhoC a c (a * Real.cos θ) = 2 * fC a c θ

a sin θ · ρ_c(a cos θ) = 2 fC θ on [0, π].

theorem Zeta32.Analytic.EnergyI.image_cos_Ioo {a : ℝ} (ha : 0 < a) : (fun (θ : ℝ) => a * Real.cos θ) '' Set.Ioo 0 Real.pi = Set.Ioo (-a) a

theorem Zeta32.Analytic.EnergyI.injOn_cos_Ioo {a : ℝ} (ha : 0 < a) : Set.InjOn (fun (θ : ℝ) => a * Real.cos θ) (Set.Ioo 0 Real.pi)

theorem Zeta32.Analytic.EnergyI.fC_two_pi_sub (a c θ : ℝ) : fC a c (2 * Real.pi - θ) = fC a c θ

theorem Zeta32.Analytic.EnergyI.integral_rhoC_eq {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (φ : ℝ → ℝ) (hφ : IntervalIntegrable (fun (θ : ℝ) => φ (a * Real.cos θ) * fC a c θ) MeasureTheory.volume 0 Real.pi) : ∫ (t : ℝ) in -a..a, φ t * rhoC a c t = ∫ (θ : ℝ) in 0..2 * Real.pi, φ (a * Real.cos θ) * fC a c θ

Change of variables t = a cos θ for the component density.