Documentation

LeanPool.Zeta5Irrational.Table.Bracket

Bracket: certified bounds for the zeta(5) proof #

source
theorem Zeta5Irrational.V_br :
236122014583635193 / 40000000000000000000 - 6 * (3 / 40) * -(5576823552816418281887 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (769448367338577 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 38396760876845215791 / 500000000000000000000) - 6 * (2 * (772599247056886688553 / 2000000000000000000000)))) ≤ Real.log (1 + qm) - 6 * (3 / 40) * Real.log (qp + (3 / 40) ^ 2) - 2 + 12 * (3 / 40) + 2 * √qp * Pfun √qm