TracialSpectralTest.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construction of the actual operator tested by the free-corner argument. Its norm and Fourier matrix are conclusions from the elementary published creation model and the local spectral arc, rather than input estimates.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.exists_actual_spectral_test line 45

Source documentation

A spectral arc supplies an actual small corner operator with the precise finite Hankel compression required by propagation.

theorem exists_actual_spectral_test
    (K : StarSubalgebra ℂ (CStarCorner p hp))
    [IsClosed (K : Set (CStarCorner p hp))]
    (hK : (factorAlgebra DA CA).topologicalClosure = K)
    (compression : RicardXuCompressionInput ((G.halfCornerGeometry dU hp htp).baseGeometry K)
      ((DA).comap K.subtype) ((CA).comap K.subtype))
    (E : TracialExpectation G.trace A) (EC : TracialExpectation G.trace C)
    (hCR : C ≤ R) (hDR : D ≤ R) (hfaithful : Function.Injective G.vector)
    (hdC : (d : P) ∈ C) (hsC : (s : P) ∈ C)
    (hdense : ∀ x, x ∈ R → G.vector x ∈ (Submodule.span ℂ
      (G.vector '' (StarAlgebra.adjoin ℂ ((D : Set P) ∪ {(s : P)}) : Set P))).topologicalClosure)
    (hpower : ∀ j : ℤ, (↑((dU * sU) ^ j) : P) ∈ C)
…

Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra, OAI.KadisonSimilarity.RicardXuCompressionInput, OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry, OAI.KadisonSimilarity.TracialExpectation