{T P : E →ₗ[ℂ] E} {s : String} {d : CertificateData} {lo : ℚ} (hd : parseCertificate s = some d) (hs : ndjsonLower s = some lo) (hpos : 0 < lo) (hEven : sectorGround T P 1 ≤...
ProvedBookProof.SirkCertificateReader.gap_pos_of_ndjsonsirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkCertificateReader.gap_pos_of_ndjson (module BookProof.SirkCertificateReader), source chapter BookProof/ChapterSirkCertificateReader.lean.
Preamble
-- Generated from ChapterSirkCertificateReader.lean — theorem BookProof.SirkCertificateReader.gap_pos_of_ndjson
import Mathlib
import Definitions.Def_ChapterSirkCertificateReader
open BookProof.SirkCertificateReader
open BookProof.SirkCertifiedGap
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]Formal statement
theorem BookProof.SirkCertificateReader.gap_pos_of_ndjson {T P : E →ₗ[ℂ] E} {s : String} {d : CertificateData} {lo : ℚ}
(hd : parseCertificate s = some d) (hs : ndjsonLower s = some lo) (hpos : 0 < lo)
(hEven : sectorGround T P 1 ≤ ((d.even.theta.toQ : ℚ) : ℝ) + ((d.even.delta.toQ : ℚ) : ℝ))
(hOdd : ((d.odd.theta.toQ : ℚ) : ℝ) - ((d.odd.delta.toQ : ℚ) : ℝ) ≤ sectorGround T P (-1)) :
sectorGround T P 1 < sectorGround T P (-1) := by sorrySource