{T P : E →ₗ[ℂ] E} {thetaE thetaO deltaE deltaO : ℕ → ℝ} {m : ℕ} (hEven : sectorGround T P 1 ≤ thetaE m + deltaE m) (hOdd : thetaO m - deltaO m ≤ sectorGround T P (-1)) (hpos : 0 < certifiedGap...
ProvedBookProof.SirkCertifiedGap.certifiedGap_soundsirkspectral-theorytimepiece
Lean 4 theorem BookProof.SirkCertifiedGap.certifiedGap_sound (module BookProof.SirkCertifiedGap), source chapter BookProof/ChapterSirkCertifiedGap.lean.
Preamble
-- Generated from ChapterSirkCertifiedGap.lean — theorem BookProof.SirkCertifiedGap.certifiedGap_sound
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.certifiedGap_sound {T P : E →ₗ[ℂ] E} {thetaE thetaO deltaE deltaO : ℕ → ℝ} {m : ℕ}
(hEven : sectorGround T P 1 ≤ thetaE m + deltaE m)
(hOdd : thetaO m - deltaO m ≤ sectorGround T P (-1))
(hpos : 0 < certifiedGap thetaE thetaO deltaE deltaO m) :
certifiedGap thetaE thetaO deltaE deltaO m
≤ sectorGround T P (-1) - sectorGround T P 1
∧ sectorGround T P 1 < sectorGround T P (-1) := by sorrySource