Shared definitions for the analytic constant F* of layout (4,5,3) (the proof notes, 5.3 (8′), the proof notes, 5.4). Mathlib only. FstarPoints implies FstarInput, which the energy bound uses.

noncomputable def Zeta32.Wt (x : ℝ) : ℝ

W(x) = (2/3)(πx − 2(x·atan(1/x) + log(1+x²)/2) + (x·atan(5/x) + 5·log(1+x²/25)/2)/2).

Equations

• Zeta32.Wt x = 2 / 3 * (Real.pi * x - 2 * (x * Real.arctan (1 / x) + Real.log (1 + x ^ 2) / 2) + (x * Real.arctan (5 / x) + 5 * Real.log (1 + x ^ 2 / 25) / 2) / 2)

noncomputable def Zeta32.Gfun (a c x : ℝ) : ℝ

G(c,x) = log((√(c²+a²) + √(a²−x²)) / (√(c²+a²) − √(a²−x²))).

Equations

• Zeta32.Gfun a c x = Real.log ((√(c ^ 2 + a ^ 2) + √(a ^ 2 - x ^ 2)) / (√(c ^ 2 + a ^ 2) - √(a ^ 2 - x ^ 2)))

noncomputable def Zeta32.rhoA (a x : ℝ) : ℝ

ρ_a(x), g = (1/3, 5/3, 4/3) on (0,1), [1,5), [5,∞).

Equations

• Zeta32.rhoA a x = (1 / 3 * (Zeta32.Gfun a 0 x - Zeta32.Gfun a 1 x) + 5 / 3 * (Zeta32.Gfun a 1 x - Zeta32.Gfun a 5 x) + 4 / 3 * Zeta32.Gfun a 5 x) / (4 * Real.pi)

noncomputable def Zeta32.massA (a : ℝ) : ℝ

Total mass of ρ_a.

Equations

• Zeta32.massA a = (1 / 3 * (1 - (√(1 + a ^ 2) - a)) + 5 / 3 * (4 - (√(25 + a ^ 2) - √(1 + a ^ 2))) + 4 / 3 * (√(25 + a ^ 2) - 5)) / 2

noncomputable def Zeta32.Jfun (a c : ℝ) : ℝ

J(c) = −c·log(2c/(c+√(c²+a²))) − (√(c²+a²) − c); J(0) = −a for a > 0.

Equations

• Zeta32.Jfun a c = -c * Real.log (2 * c / (c + √(c ^ 2 + a ^ 2))) - (√(c ^ 2 + a ^ 2) - c)

noncomputable def Zeta32.ellA (a : ℝ) : ℝ

ℓ(a), the closed form (16) of GLOBAL-INTEGRAL-v1 for this layout.

Equations

• Zeta32.ellA a = 2 * Real.log (a / 2) + 1 / 3 * (Zeta32.Jfun a 0 - Zeta32.Jfun a 1) + 5 / 3 * (Zeta32.Jfun a 1 - Zeta32.Jfun a 5) + 4 / 3 * Zeta32.Jfun a 5

def Zeta32.FstarInput : Prop

The analytic constant is at most −6 at the root of the mass equation.

Equations

• Zeta32.FstarInput = ∀ (a : ℝ), 0 < a → Zeta32.massA a = 1 → 9 * (3 / 2 - Real.log 3) + 9 / 2 * (Zeta32.ellA a - 2 * ∫ (x : ℝ) in 0..a, Zeta32.Wt x * Zeta32.rhoA a x) ≤ -6

noncomputable def Zeta32.aMinus : ℝ

Rational lower endpoint for the equilibrium-support parameter.

Equations

• Zeta32.aMinus = 93331 / 50000

noncomputable def Zeta32.aPlus : ℝ

Rational upper endpoint for the equilibrium-support parameter.

Equations

• Zeta32.aPlus = 186663 / 100000

noncomputable def Zeta32.xk (k : ℕ) : ℝ

x_k = a₋·k/16.

Equations

• Zeta32.xk k = Zeta32.aMinus * ↑k / 16

def Zeta32.Wlow : Fin 15 → ℚ

Certified rational lower bounds for the potential weight at the fifteen test points.

Equations

• Zeta32.Wlow = ![17 / 250, 153 / 1000, 127 / 500, 369 / 1000, 499 / 1000, 641 / 1000, 397 / 500, 239 / 250, 141 / 125, 1307 / 1000, 1493 / 1000, 421 / 250, 1881 / 1000, 2083 / 1000, 286 / 125]

def Zeta32.Rlow : Fin 15 → ℚ

Certified rational lower bounds for the auxiliary ratio at the fifteen test points.

Equations

• Zeta32.Rlow = ![223 / 500, 203 / 500, 377 / 1000, 44 / 125, 329 / 1000, 153 / 500, 283 / 1000, 13 / 50, 119 / 500, 43 / 200, 191 / 1000, 167 / 1000, 71 / 500, 113 / 1000, 39 / 500]

def Zeta32.FstarPoints : Prop

Finitely many rational checks. Index k : Fin 15 stands for the point x_(k+1).

Equations

• One or more equations did not get rendered due to their size.