TracialRepeatedWords.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Realize the abstract propagation data by actual tracial left multipliers. The remaining word data are elementary reduced-word multiplication and isometry identities; the scaled support and vanishing coefficient are proved.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.embedded_left_scaled_initial line 24
Source documentation
A scaled initial projection in the algebra gives the corresponding operator identity in any represented tracial Hilbert space.
```
theorem embedded_left_scaled_initial (G : TracialCornerGeometry P H)
    (ι : D →⋆ₐ[ℂ] P) (x q : D) (c : ℂ) (hx : star x * x = c • q) :
    (G.left (ι x)).adjoint.comp (G.left (ι x)) = c • G.left (ι q) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry
structure OAI.KadisonSimilarity.TracialRepeatedWordRealization line 42
Source documentation
The remaining raw reduced-word geometry for a fixed positive degree. All operators acting on the ambient space are specified as left multipliers. There is no approximation estimate among these fields.
```
structure TracialRepeatedWordRealization where
…
```
def OAI.KadisonSimilarity.TracialRepeatedWordRealization.propagationData line 64
Source documentation
The full abstract propagation data are derived from the raw word realization and the actual corner Haar unitary.
```
def propagationData (hτ : GD.trace 1 = 1) (ha : 0 < a)
    (htrace : GD.trace q = (a : ℂ)) (hhaar : HaarCornerMoments GD.trace z a) :
    RepeatedLetterWords (E := E) (F := F) Y B₀ Bₖ W.vacuum a where
…
```
Mentions: OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.RepeatedLetterWords
theorem OAI.KadisonSimilarity.TracialRepeatedWordRealization.exceptional_coefficient_tendsto_zero line 92
Source documentation
Every fixed error vector has a vanishing exceptional coefficient; this is a conclusion of Haar orthogonality and the head tensor representation.
```
theorem exceptional_coefficient_tendsto_zero (hτ : GD.trace 1 = 1) (ha : 0 < a)
    (htrace : GD.trace q = (a : ℂ)) (hhaar : HaarCornerMoments GD.trace z a) (y : H) :
    Filter.Tendsto (fun n => W.vacuum.starProjection
      (G.left (ι (haarCornerLetter z a n)) y)) Filter.atTop (nhds 0) :=
…
```
Mentions: OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.haarCornerLetter

theorem OAI.KadisonSimilarity.TracialRepeatedWordRealization.propagation line 101

Source documentation

A supported column approximation propagates to the repeated word with factor two. All action-commutation and exceptional-limit requirements have been discharged in the tracial model.

theorem propagation (hτ : GD.trace 1 = 1) (ha : 0 < a)
    (htrace : GD.trace q = (a : ℂ)) (hhaar : HaarCornerMoments GD.trace z a)
    (r b : P) {η : ℝ}
    (hcolumn : ‖(Y - G.right b).comp (G.corner 1 r).toSubmodule.subtypeL‖ ≤ η)
    (v : B) (hv : R.small v ∈ (G.corner 1 r).toSubmodule) :
    ‖Bₖ (R.repeatVector v) - R.repeatVector (B₀ v)‖ ≤ 2 * η * ‖v‖ := by
…

Mentions: OAI.KadisonSimilarity.HaarCornerMoments