Definitions for the energy estimate of the proof notes, §5.3 (layout (4,5,3), c = 3).

• potD ρ a x = ∫_{-a}^{a} log|x - t| ρ(t) dt and ID ρ a = ∫ potD ρ a · ρ (logarithmic potential and energy of a density on [-a, a]), potA a = potD (rhoA a) a, IA a = ID (rhoA a) a for the closed form rhoA of FstarDefs;
• the c-components of the proof notes (8′): rhoC a c t = c√(a²-t²)/(2π u_c (t²+c²)), u_c = √(c²+a²), the weight gtil = (1/3, 5/3, 4/3) on (0,1), [1,5), [5,∞), and the constants kC a c, wC c x with 2 L_c = kC + wC on the support.

noncomputable def Zeta32.Analytic.EnergyI.potD (ρ : ℝ → ℝ) (a x : ℝ) : ℝ

Logarithmic potential of a density ρ supported on [-a, a].

Equations

• Zeta32.Analytic.EnergyI.potD ρ a x = ∫ (t : ℝ) in -a..a, Real.log |x - t| * ρ t

noncomputable def Zeta32.Analytic.EnergyI.ID (ρ : ℝ → ℝ) (a : ℝ) : ℝ

Logarithmic energy of a density ρ supported on [-a, a].

Equations

• Zeta32.Analytic.EnergyI.ID ρ a = ∫ (x : ℝ) in -a..a, Zeta32.Analytic.EnergyI.potD ρ a x * ρ x

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

Potential of the comparison density rhoA a.

Equations

• Zeta32.Analytic.EnergyI.potA a x = Zeta32.Analytic.EnergyI.potD (Zeta32.rhoA a) a x

noncomputable def Zeta32.Analytic.EnergyI.IA (a : ℝ) : ℝ

Energy of the comparison density rhoA a.

Equations

• Zeta32.Analytic.EnergyI.IA a = Zeta32.Analytic.EnergyI.ID (Zeta32.rhoA a) a

noncomputable def Zeta32.Analytic.EnergyI.gtil (c : ℝ) : ℝ

The weight g of the proof notes (8′) for layout (4,5,3).

Equations

• Zeta32.Analytic.EnergyI.gtil c = if c < 1 then 1 / 3 else if c < 5 then 5 / 3 else 4 / 3

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

u_c = √(c² + a²).

Equations

• Zeta32.Analytic.EnergyI.uC a c = √(c ^ 2 + a ^ 2)

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

The component density ρ_c of GLOBAL-INTEGRAL-v1 (9).

Equations

• Zeta32.Analytic.EnergyI.rhoC a c t = c * √(a ^ 2 - t ^ 2) / (2 * Real.pi * Zeta32.Analytic.EnergyI.uC a c * (t ^ 2 + c ^ 2))

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

Potential of the component ρ_c.

Equations

• Zeta32.Analytic.EnergyI.potC a c x = ∫ (t : ℝ) in -a..a, Real.log |x - t| * Zeta32.Analytic.EnergyI.rhoC a c t

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

Value of 2 L_c − wC c on the support.

Equations

• Zeta32.Analytic.EnergyI.kC a c = Real.log (a * c / (Zeta32.Analytic.EnergyI.uC a c + c)) - c / Zeta32.Analytic.EnergyI.uC a c * Real.log (a / 2)

noncomputable def Zeta32.Analytic.EnergyI.wC (c x : ℝ) : ℝ

w_c(x) = ½ log(1 + x²/c²), so that W = ∫ g w_c dc.

Equations

• Zeta32.Analytic.EnergyI.wC c x = Real.log (1 + x ^ 2 / c ^ 2) / 2