The comparison measure of Appendix A and the constants of Section 6

λ, α, C* (6.3), M₀ (6.2), Table 1 (the sixteen arcsine components of ρ), the partial sums S_j, and the energy I(ρ) by formula (A.2).

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.lam : ℝ

λ = 37/40.

Equations

• Zeta5Irrational.lam = 37 / 40

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.alph : ℝ

α = 3/40.

Equations

• Zeta5Irrational.alph = 3 / 40

noncomputable def Zeta5Irrational.Cstar : ℝ

The constant C* of (6.3).

Equations

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

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.M0 : ℝ

M₀ = -1329/200 of (6.2).

Equations

• Zeta5Irrational.M0 = -1329 / 200

def Zeta5Irrational.table1 : List (ℕ × ℕ × ℕ)

Table 1: 10¹² a_j, 10¹² b_j, 10¹² c_j.

Equations

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

noncomputable def Zeta5Irrational.aρ (j : ℕ) : ℝ

a_j, b_j, c_j (1-indexed; 0 outside the table).

Equations

• Zeta5Irrational.aρ j = ↑(Zeta5Irrational.table1.getD (j - 1) (0, 0, 0)).1 / 10 ^ 12

noncomputable def Zeta5Irrational.bρ (j : ℕ) : ℝ

Right endpoint of the jth arcsine component, read from the exact rational table.

Equations

• Zeta5Irrational.bρ j = ↑(Zeta5Irrational.table1.getD (j - 1) (0, 0, 0)).2.1 / 10 ^ 12

noncomputable def Zeta5Irrational.cρ (j : ℕ) : ℝ

Mass of the jth arcsine component, read from the exact rational table.

Equations

• Zeta5Irrational.cρ j = ↑(Zeta5Irrational.table1.getD (j - 1) (0, 0, 0)).2.2 / 10 ^ 12

noncomputable def Zeta5Irrational.Sρ (j : ℕ) : ℝ

Partial sums S_j = ∑_{i ≤ j} c_i.

Equations

• Zeta5Irrational.Sρ j = ∑ i ∈ Finset.Icc 1 j, Zeta5Irrational.cρ i

noncomputable def Zeta5Irrational.Irho : ℝ

The logarithmic energy I(ρ) of the measure ρ, formula (A.2).

Equations

• Zeta5Irrational.Irho = ∑ j ∈ Finset.Icc 1 16, (Zeta5Irrational.Sρ j ^ 2 - Zeta5Irrational.Sρ (j - 1) ^ 2) * Real.log ((Zeta5Irrational.bρ j - Zeta5Irrational.aρ j) / 4)

theorem Zeta5Irrational.Sρ_sixteen : Sρ 16 = lam

The total mass of ρ is λ (Appendix A.1).