TracialHeadCoordinates.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The exceptional projection in propagation, constructed from the tracial head of the reduced-word decomposition and actual corner Haar powers.

structure OAI.KadisonSimilarity.TracialHeadCoordinates line 20
Source documentation
Grouping reduced words by their possible initial D letter yields these coordinates. The sole action field is ordinary left multiplication on that initial tensor factor; no propagation estimate is included.
```
structure TracialHeadCoordinates (GD : TracialCornerGeometry D E)
    (G : TracialCornerGeometry P H) (ι : D →⋆ₐ[ℂ] P) (F : Type*)
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] where
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry
theorem OAI.KadisonSimilarity.TracialCornerGeometry.left_adjoint_traceVector line 31
Source documentation
The adjoint of left multiplication has the expected value on the trace vector, providing the slicing vector without an additional hypothesis.
```
theorem left_adjoint_traceVector (G : TracialCornerGeometry P H) (a : P) :
    (G.left a).adjoint (G.vector 1) = G.vector (star a) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry
abbrev OAI.KadisonSimilarity.TracialHeadCoordinates.vacuum line 44
Source documentation
The actual exceptional subspace consists of words whose initial D coordinate is the scalar trace vector.
```
abbrev vacuum : Submodule ℂ H := tracialVacuumSubspace W.unitary (GD.vector 1)
```
Mentions: OAI.KadisonSimilarity.tracialVacuumSubspace
theorem OAI.KadisonSimilarity.TracialHeadCoordinates.vacuum_hasOrthogonalProjection line 48
Source documentation
Orthogonal projection onto the exceptional subspace exists by the tensor coordinates and trace normalization.
```
theorem vacuum_hasOrthogonalProjection (hτ : GD.trace 1 = 1) :
    W.vacuum.HasOrthogonalProjection := by
…
```
theorem OAI.KadisonSimilarity.TracialHeadCoordinates.vacuum_slice line 57
Source documentation
The exceptional component after a left letter is the tensor slice against its adjoint applied to the trace vector.
```
theorem vacuum_slice (hτ : GD.trace 1 = 1) (d : D) (z : H) :
    W.vacuum.starProjection (G.left (ι d) z) =
      W.unitary.symm (hilbertTensorInsert (GD.vector 1)
        (tensorSlice (GD.vector (star d)) (W.unitary z))) := by
…
```
Mentions: OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tensorSlice

theorem OAI.KadisonSimilarity.TracialHeadCoordinates.vacuum_tendsto_zero line 71

Source documentation

A weakly null sequence of adjoint trace vectors has a vanishing exceptional component on each fixed ambient vector.

theorem vacuum_tendsto_zero (hτ : GD.trace 1 = 1) (x : ℕ → D)
    (hx : Orthonormal ℂ (fun n => GD.vector (star (x n)))) (z : H) :
    Filter.Tendsto (fun n => W.vacuum.starProjection (G.left (ι (x n)) z))
      Filter.atTop (nhds 0) := by
…

theorem OAI.KadisonSimilarity.TracialHeadCoordinates.haar_vacuum_tendsto_zero line 85

Source documentation

The normalized powers of an actual Haar unitary in a corner of D therefore satisfy the exceptional-component limit used in propagation.

theorem haar_vacuum_tendsto_zero (hτ : GD.trace 1 = 1)
    {q : D} {hq : IsStarProjection q} (u : _root_.unitary (CStarCorner q hq))
    {a : ℝ} (ha : 0 < a) (htrace : GD.trace q = (a : ℂ))
    (hhaar : HaarCornerMoments GD.trace u a) (z : H) :
    Filter.Tendsto (fun n => W.vacuum.starProjection
      (G.left (ι (haarCornerLetter u a n)) z)) Filter.atTop (nhds 0) :=
…

Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.haarCornerLetter