TracialSpectralNorm.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The narrow spectral arc has the required small norm in the original algebra. Its creation model is applied on the closed algebra generated by the two corner factors, with the normalized restricted trace.

instance OAI.KadisonSimilarity.CStarCorner.isClosed_subalgebra line 19
def OAI.KadisonSimilarity.TracialCornerGeometry.halfCornerGeometry line 36
Source documentation
This is the ordinary normalized corner geometry before restriction to the algebra generated by its two free factors.
```
def halfCornerGeometry :
    TracialCornerGeometry (CStarCorner (dihedralHalfProjection d) hp)
      (G.corner (dihedralHalfProjection d) (dihedralHalfProjection d)) :=
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.dihedralHalfProjection

theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_spectral_arc_compression line 48

Source documentation

The published elementary creation model yields the actual 3u norm bound for the spectral test, with u = 2t.

theorem norm_spectral_arc_compression
    (hS : (factorAlgebra (CStarCorner.subalgebra (dihedralHalfProjection d) hp D hpD)
      (CStarCorner.subalgebra (dihedralHalfProjection d) hp C hpC)).topologicalClosure = S)
    (published : RicardXuCompressionInput
      ((G.halfCornerGeometry d hp htp).baseGeometry S)
      ((CStarCorner.subalgebra (dihedralHalfProjection d) hp D hpD).comap S.subtype)
      ((CStarCorner.subalgebra (dihedralHalfProjection d) hp C hpC).comap S.subtype))
    (hfaithful : Function.Injective G.vector)
    (hfree : ScalarFree (CStarCorner.normalizedTrace (dihedralHalfProjection d) hp G.trace)
      (CStarCorner.subalgebra (dihedralHalfProjection d) hp D hpD)
      (CStarCorner.subalgebra (dihedralHalfProjection d) hp C hpC))
    (hdC : (d : P) ∈ C)
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra, OAI.KadisonSimilarity.CStarCorner.subalgebra, OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.RicardXuCompressionInput, OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CStarCorner.normalizedTrace