Numerical constants of the paper

U of (6.4), A* of (5.19), A_M of (5.20), the displayed value A₂₀₀ of Appendix B.3, the identity (5.20) at M = 200 and the margin (7.2), both checked by norm_num.

def Zeta5Irrational.U : ℚ

The constant U of Lemma 6.1 / (6.4).

Equations

• Zeta5Irrational.U = -2733991 / 2000000

def Zeta5Irrational.Astar : ℚ

The constant A* of (5.19).

Equations

• Zeta5Irrational.Astar = 9928298118277006344769 / 7535670527041937280000

def Zeta5Irrational.A (M : ℚ) : ℚ

A_M of (5.20), with λ = 37/40.

Equations

• Zeta5Irrational.A M = Zeta5Irrational.Astar + 7 * (37 / 40) / M - (2923 / 240 - 1 / 4) / M ^ 2 + 32 / M ^ 3

def Zeta5Irrational.A200 : ℚ

The value A₂₀₀ displayed in Appendix B.3.

Equations

• Zeta5Irrational.A200 = 127125602969131786927559 / 94195881588024216000000

theorem Zeta5Irrational.A_200_eq : A 200 = A200

theorem Zeta5Irrational.margin : 139 / 5 < -1600 * (A200 + U)

The rational margin (7.2): -1600 (A₂₀₀ + U) > 139 / 5.

def Zeta5Irrational.Aeff : ℚ

The normalisation constant proved here (Zeta5Irrational.Growth): limsup K⁻² log m_K ≤ A_eff. It is weaker than the paper's A₂₀₀, but still below -U.

Equations

• Zeta5Irrational.Aeff = 136 / 100

theorem Zeta5Irrational.Aeff_margin : Aeff + U < 0

The margin used for irrationality: A_eff + U < 0.

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.Kr (n : ℕ) : ℝ

K = 40 n as a real number.

Equations

• Zeta5Irrational.Kr n = 40 * ↑n