Potential of the component ρ_c (the proof notes (8′), per component):

2 L_c(x) = kC a c + wC c x   (|x| ≤ a),        2 L_c(x) ≤ kC a c + wC c x   (all x).

Proof: with t = a cos θ, x − a cos θ = −(a/(2e))(e − q₁)(e − q₂) on the unit circle, q₁q₂ = 1, q₁ + q₂ = 2x/a; the Poisson formula for log|· − q| evaluates the balayage part and Jensen's formula the arcsine part. Outside [-a, a] the inequality reduces to ψ(q) ≥ 0 for q ≥ 1, proved by ψ′ ≥ 0.

theorem Zeta32.Analytic.EnergyI.circleMap_zero_one_eq (θ : ℝ) : circleMap 0 1 θ = { re := Real.cos θ, im := Real.sin θ }

theorem Zeta32.Analytic.EnergyI.norm_mul_norm_circle (q1 q2 : ℂ) (ξ : ℝ) (hs : q1 + q2 = 2 * ↑ξ) (hp : q1 * q2 = 1) (θ : ℝ) : ‖circleMap 0 1 θ - q1‖ * ‖circleMap 0 1 θ - q2‖ = 2 * |Real.cos θ - ξ|

On the unit circle, |e − q₁||e − q₂| = 2|cos θ − ξ| when q₁ + q₂ = 2ξ, q₁q₂ = 1.

theorem Zeta32.Analytic.EnergyI.log_abs_decomp {a : ℝ} (x : ℝ) (q1 q2 : ℂ) (ha : 0 < a) (hs : q1 + q2 = 2 * ↑(x / a)) (hp : q1 * q2 = 1) {θ : ℝ} (hθ : a * Real.cos θ ≠ x) : Real.log |x - a * Real.cos θ| = Real.log (a / 2) + Real.log ‖circleMap 0 1 θ - q1‖ + Real.log ‖circleMap 0 1 θ - q2‖

theorem Zeta32.Analytic.EnergyI.ae_log_abs_decomp {a : ℝ} (x : ℝ) (q1 q2 : ℂ) (ha : 0 < a) (hs : q1 + q2 = 2 * ↑(x / a)) (hp : q1 * q2 = 1) : ∀ᵐ (θ : ℝ), Real.log |x - a * Real.cos θ| = Real.log (a / 2) + Real.log ‖circleMap 0 1 θ - q1‖ + Real.log ‖circleMap 0 1 θ - q2‖

noncomputable def Zeta32.Analytic.EnergyI.Lx (a x θ : ℝ) : ℝ

L_x(θ) = log|x − a cos θ|.

Equations

• Zeta32.Analytic.EnergyI.Lx a x θ = Real.log |x - a * Real.cos θ|

theorem Zeta32.Analytic.EnergyI.PK_betaC_norm {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (b : ℝ) (hb : b = betaC a c ∨ b = -betaC a c) : ‖Complex.I * ↑b‖ < 1

theorem Zeta32.Analytic.EnergyI.potC_eq_theta {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (x : ℝ) (hL : IntervalIntegrable (Lx a x) MeasureTheory.volume 0 (2 * Real.pi)) : potC a c x = ∫ (θ : ℝ) in 0..2 * Real.pi, Lx a x θ * fC a c θ

L_c in angular form.

theorem Zeta32.Analytic.EnergyI.integral_Lx_fC {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (x : ℝ) (hL : IntervalIntegrable (Lx a x) MeasureTheory.volume 0 (2 * Real.pi)) : ∫ (θ : ℝ) in 0..2 * Real.pi, Lx a x θ * fC a c θ = ((1 / (8 * Real.pi) * ∫ (θ : ℝ) in 0..2 * Real.pi, Lx a x θ * PK (Complex.I * ↑(betaC a c)) θ) + 1 / (8 * Real.pi) * ∫ (θ : ℝ) in 0..2 * Real.pi, Lx a x θ * PK (Complex.I * ↑(-betaC a c)) θ) - c / uC a c / (4 * Real.pi) * ∫ (θ : ℝ) in 0..2 * Real.pi, Lx a x θ

Linear decomposition of ∫ L_x fC through the Poisson form of fC.

theorem Zeta32.Analytic.EnergyI.log_norm_pair_iβ (β ξ : ℝ) (q1 q2 : ℂ) (hs : q1 + q2 = 2 * ↑ξ) (hp : q1 * q2 = 1) (b : ℝ) (hb : b = β ∨ b = -β) (hβ : β ^ 2 < 1) : Real.log ‖Complex.I * ↑b - q1‖ + Real.log ‖Complex.I * ↑b - q2‖ = Real.log ((1 - β ^ 2) ^ 2 + 4 * β ^ 2 * ξ ^ 2) / 2

log‖w − q₁‖ + log‖w − q₂‖ = ½ log|w² − 2ξw + 1|² evaluated at w = ±iβ.

theorem Zeta32.Analytic.EnergyI.psi_nonneg {κ β q : ℝ} (hβ : 0 < β) (hκ0 : 0 ≤ κ) (hκ : κ * (1 + β ^ 2) = 1 - β ^ 2) (hq : 1 ≤ q) : Real.log (q ^ 2 + β ^ 2) / 2 - Real.log (β ^ 2 * q ^ 2 + 1) / 2 ≤ κ * Real.log q

ψ(q) = κ log q − ½ log(q² + β²) + ½ log(β²q² + 1) ≥ 0 for q ≥ 1 when κ(1+β²) = 1 − β².

theorem Zeta32.Analytic.EnergyI.rhoC_neg (a c t : ℝ) : rhoC a c (-t) = rhoC a c t

theorem Zeta32.Analytic.EnergyI.potC_neg (a c x : ℝ) : potC a c (-x) = potC a c x

theorem Zeta32.Analytic.EnergyI.wC_neg (c x : ℝ) : wC c (-x) = wC c x

theorem Zeta32.Analytic.EnergyI.two_potC_inside {a c : ℝ} (ha : 0 < a) (hc : 0 < c) {x : ℝ} (hx : |x| ≤ a) : 2 * potC a c x = kC a c + wC c x

Inside the support: 2 L_c(x) = kC + wC.

theorem Zeta32.Analytic.EnergyI.key_alg_out (L Lq Lb κ : ℝ) : 2 * (1 / (8 * Real.pi) * (2 * Real.pi * (L - Lq + 2 * (Lb / 2))) + 1 / (8 * Real.pi) * (2 * Real.pi * (L - Lq + 2 * (Lb / 2))) - κ / (4 * Real.pi) * (2 * Real.pi * (L + Lq))) = L - Lq + Lb - κ * (L + Lq)

theorem Zeta32.Analytic.EnergyI.two_potC_outside_pos {a c : ℝ} (ha : 0 < a) (hc : 0 < c) {x : ℝ} (hx : a < x) : 2 * potC a c x ≤ kC a c + wC c x

Outside the support (x > a): 2 L_c(x) ≤ kC + wC.

theorem Zeta32.Analytic.EnergyI.two_potC_le {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (x : ℝ) : 2 * potC a c x ≤ kC a c + wC c x