: richardson qymG4L3 qymG4L4 3 4 2 = 27999423 / 3500000
ProvedBookProof.SirkGapTable.richardson_qym_g4sirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkGapTable.richardson_qym_g4 (module BookProof.SirkGapTable), source chapter BookProof/ChapterSirkGapTable.lean.
Preamble
-- Generated from ChapterSirkGapTable.lean — theorem BookProof.SirkGapTable.richardson_qym_g4
import Mathlib
import Definitions.Def_ChapterSirkGapTable
open BookProof.SirkGapTable
noncomputable section
open BookProof.SirkCertifiedGap
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
open RealFormal statement
theorem BookProof.SirkGapTable.richardson_qym_g4 :
richardson qymG4L3 qymG4L4 3 4 2 = 27999423 / 3500000 := by sorrySource