: qcdG2M4.lower = 1.932
ProvedBookProof.SirkCertifiedGap.qcdG2M4_lowersirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkCertifiedGap.qcdG2M4_lower (module BookProof.SirkCertifiedGap), source chapter BookProof/ChapterSirkCertifiedGap.lean.
Preamble
-- Generated from ChapterSirkCertifiedGap.lean — theorem BookProof.SirkCertifiedGap.qcdG2M4_lower
import Mathlib
import Definitions.Def_ChapterSirkCertifiedGap
open BookProof.SirkCertifiedGap
noncomputable section
open scoped InnerProductSpace
open Finset Filter Topology
open BookProof.SirkFinitePrecision
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E]Formal statement
theorem BookProof.SirkCertifiedGap.qcdG2M4_lower : qcdG2M4.lower = 1.932 := by sorry
Source