TracialWordBase.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The vacuum endpoint in degree zero is the actual base Hilbert space. Consequently the repeated-word action implies base-space invariance; this is not an additional assumption on the symmetrized operator.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_baseVector_one line 22
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracial_baseWordInclusion_vector line 43
Source documentation
The empty-word formula identifies the abstract vacuum inclusion.
```
theorem tracial_baseWordInclusion_vector (b : A) :
    baseWordInclusion (G.baseVector A 1) U (G.baseVector D 1)
      (G.norm_baseVector_one D hτ) (G.baseVector A b) = G.vector (b : P) := by
…
```
Mentions: OAI.KadisonSimilarity.baseWordInclusion
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracial_baseWordInclusion_eq line 56
Source documentation
Equality extends to the completed base space by density.
```
theorem tracial_baseWordInclusion_eq :
    baseWordInclusion (G.baseVector A 1) U (G.baseVector D 1)
      (G.norm_baseVector_one D hτ) = G.baseInclusion A :=
…
```
Mentions: OAI.KadisonSimilarity.baseWordInclusion
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_invariant_of_word_action line 63
Source documentation
A degree-zero repeated action gives invariance of the actual base space.
```
theorem baseSpace_invariant_of_word_action (Y : H →L[ℂ] H)
    (T : WordMultiplicity (G.baseVector A 1) 0 →L[ℂ]
      WordMultiplicity (G.baseVector A 1) 0)
    (hY : ∀ v, Y (U.inclusion 0 (hilbertTensorInsert v
        (emptyEndpoint (F := centeredSubspace (G.baseVector D 1)) (G.baseVector D 1)))) =
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.emptyEndpoint, OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseOperator_of_word_action line 80
Source documentation
The same word action identifies its multiplicity-zero coefficient with the actual compression used in the commutator estimate.
```
theorem baseOperator_of_word_action (Y : H →L[ℂ] H)
    (T : WordMultiplicity (G.baseVector A 1) 0 →L[ℂ]
      WordMultiplicity (G.baseVector A 1) 0)
    (hY : ∀ v, Y (U.inclusion 0 (hilbertTensorInsert v
        (emptyEndpoint (F := centeredSubspace (G.baseVector D 1)) (G.baseVector D 1)))) =
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.emptyEndpoint, OAI.KadisonSimilarity.centeredSubspace