OAI/Analysis/KadisonSimilarity/Tracial/TracialSpectralColumns.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialDihedralColumns_rotation_formula line 29

   Source documentation

   The repeated product column is exactly the normalized negative rotation power column; the identity is proved on its actual bounded algebra vectors.

   theorem tracialDihedralColumns_rotation_formula (N : ℕ) (i : Fin N) (a : A) :
       G.tracialDihedralColumns D A hf hτ d s e hdstar hdsq hd0 hsstar hssq hs0
         he ht hte N i (G.baseVector A a) =
         dihedralNormalization t • G.vector
           ((e : P) * (↑((dU * sU) ^ (-(i.val : ℤ))) : P) * (a : P)) := by
   …

   Mentions: OAI.KadisonSimilarity.dihedralNormalization

2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.spectral_arc_actual_columns line 43

   Source documentation

   The Fourier compression theorem, on the actual normalized columns. The bounded column formula and reflected base compression are derived here.

   theorem spectral_arc_actual_columns
       (C S : StarSubalgebra ℂ P)
       (E : TracialExpectation G.trace A) (EC : TracialExpectation G.trace C)
       (hCS : C ≤ S) (hDS : D ≤ S) (hfaithful : Function.Injective G.vector)
       (hdC : (d : P) ∈ C) (hsC : (s : P) ∈ C)
       (hdense : ∀ x, x ∈ S → G.vector x ∈ (Submodule.span ℂ
         (G.vector '' (StarAlgebra.adjoin ℂ ((D : Set P) ∪ {(s : P)}) : Set P))).topologicalClosure)
       (hpower : ∀ j : ℤ, (↑((dU * sU) ^ j) : P) ∈ C)
       (hp : IsStarProjection (dihedralHalfProjection dU))
       (hpD : dihedralHalfProjection dU ∈ D)
       (htp : G.trace (dihedralHalfProjection dU) = (1 / 2 : ℂ))
       (hfree : ScalarFree (CStarCorner.normalizedTrace (dihedralHalfProjection dU) hp G.trace)
   …

   Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CStarCorner.normalizedTrace