{T P : E →ₗ[ℂ] E} (c : GapCertificate) {thetaE thetaO deltaE deltaO : ℝ} (hgap : c.gap = thetaO - thetaE) (hwidth : c.width = deltaO + deltaE) (hEven : sectorGround T P 1 ≤ thetaE + deltaE) (hOdd...
ProvedBookProof.SirkCertifiedGap.gap_pos_of_certificatesirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkCertifiedGap.gap_pos_of_certificate (module BookProof.SirkCertifiedGap), source chapter BookProof/ChapterSirkCertifiedGap.lean.
Preamble
-- Generated from ChapterSirkCertifiedGap.lean — theorem BookProof.SirkCertifiedGap.gap_pos_of_certificate
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.gap_pos_of_certificate {T P : E →ₗ[ℂ] E} (c : GapCertificate)
{thetaE thetaO deltaE deltaO : ℝ}
(hgap : c.gap = thetaO - thetaE) (hwidth : c.width = deltaO + deltaE)
(hEven : sectorGround T P 1 ≤ thetaE + deltaE)
(hOdd : thetaO - deltaO ≤ sectorGround T P (-1))
(hpos : 0 < c.lower) :
sectorGround T P 1 < sectorGround T P (-1) := by sorrySource