PublishedWordCreation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The elementary creation part of the published reduced free-product model.

Ricard--Xu, J. reine angew. Math. 599 (2006), Section 1, pp. 2--3, and Lemma 2.3: prepending a centered letter to a word from the opposite factor is the Hilbert tensor insertion. This interface has only those raw word maps; prefix isometry and propagation are derived separately.

structure OAI.KadisonSimilarity.ReducedWordCreationModel line 26
Source documentation
Grouping ordinary reduced words by their first factor. Both the tail space and the A-leading space are actual closed subspaces of the GNS space.
```
structure ReducedWordCreationModel where
…
```
def OAI.KadisonSimilarity.RicardXuCreationInput line 40
Source documentation
Published input specialized to the two actual tracial factors.
```
def RicardXuCreationInput : Prop :=
…
```
def OAI.KadisonSimilarity.ReducedWordCreationModel.tracialCreationFormulas line 50
Source documentation
The normalized Haar letters are among the centered algebra letters in the published model, so the raw propagation formulas need no new hypothesis.
```
def tracialCreationFormulas
    (s : A) (hs : G.trace (s : P) = 0)
    {q : D} {hq : IsStarProjection q} (z : unitary (CStarCorner q hq))
    {a : ℝ} (ha : 0 < a) (htrace : G.trace (q : P) = (a : ℂ))
    (hhaar : HaarCornerMoments (G.baseGeometry D).trace z a) :
    TracialCreationFormulas G A D W.head s hs z ha htrace hhaar W.aLead.toSubmodule where
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.TracialCreationFormulas
structure OAI.KadisonSimilarity.ReducedWordCompressionModel line 72
Source documentation
The vacuum/creation coordinates for multiplication by the second factor. The projection singles out words beginning in that factor, and before is its orthogonal complement. No operator norm estimate is part of this data.
```
structure ReducedWordCompressionModel where
…
```
def OAI.KadisonSimilarity.RicardXuCompressionInput line 95
Source documentation
Section 1 and Lemma 2.3 of Ricard--Xu, restricted to one creation letter and its preceding-word space in a scalar tracial reduced product.
```
def RicardXuCompressionInput : Prop :=
…
```

theorem OAI.KadisonSimilarity.norm_narrow_compression_of_published_words line 101

Source documentation

The narrow-arc norm estimate follows from the published elementary creation model and the proved three-block estimate.

theorem norm_narrow_compression_of_published_words
    (published : RicardXuCompressionInput G A D)
    (hτ : G.trace 1 = 1) (hfaithful : Function.Injective G.vector)
    (hfree : ScalarFree G.trace D A) (hdense : ReducedWordGenerated G A D)
    (e : A) (he : IsStarProjection (e : P))
    (b : D) (hbself : star b = b) (hb0 : G.trace (b : P) = 0)
    {u : ℝ} (hu : 0 ≤ u) (hetrace : G.trace (e : P) = (u : ℂ))
    (hb₂ : (G.trace (star (b : P) * (b : P))).re ≤ u) (hbnorm : ‖(b : P)‖ ≤ 1) :
    ‖(e : P) * (b : P) * (e : P)‖ ≤ 3 * u := by
…

Mentions: OAI.KadisonSimilarity.RicardXuCompressionInput, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.ReducedWordGenerated