BaseSymmetry.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

A trace-zero symmetry of the actual base algebra supplies the normalized centered letter and its represented selfadjoint involution.

def OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetryLetter line 21
Source documentation
A trace-zero base element is an actual centered base Hilbert vector.
```
def baseSymmetryLetter (s : A) (hzero : G.trace (s : P) = 0) :
    centeredSubspace (G.baseVector A 1) :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetryLetter_coe line 27
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_baseSymmetryLetter line 32
Source documentation
Trace normalization and the symmetry relation give norm one, rather than requiring a separately chosen unit vector in the centered space.
```
theorem norm_baseSymmetryLetter (s : A) (hzero : G.trace (s : P) = 0)
    (hself : star s = s) (hsquare : s * s = 1) (htrace : G.trace 1 = 1) :
    ‖G.baseSymmetryLetter A s hzero‖ = 1 := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetry_selfadjoint line 45
Source documentation
Selfadjointness passes through the actual base representation.
```
theorem baseSymmetry_selfadjoint (s : A) (hself : star s = s) :
    IsSelfAdjoint (G.baseRepresentation A s) := by
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetry_square line 52

Source documentation

The represented base symmetry squares to the identity operator.

theorem baseSymmetry_square (s : A) (hsquare : s * s = 1) :
    (G.baseRepresentation A s).comp (G.baseRepresentation A s) =
      ContinuousLinearMap.id ℂ (G.baseSpace A) := by
…

def OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetryUnitary line 60
Source documentation
The represented symmetry is an actual unitary bounded operator.
```
def baseSymmetryUnitary (s : A) (hself : star s = s) (hsquare : s * s = 1) :
    unitary (G.baseSpace A →L[ℂ] G.baseSpace A) :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_baseSymmetry_le_one line 71
Source documentation
The unitary relation gives contractivity even if the Hilbert space were trivial; trace normalization is only needed for the centered letter's norm.
```
theorem norm_baseSymmetry_le_one (s : A) (hself : star s = s) (hsquare : s * s = 1) :
    ‖G.baseRepresentation A s‖ ≤ 1 := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetry_compression line 82
Source documentation
The compressed ambient symmetry and the restricted base representation are exactly the same operator.
```
theorem baseSymmetry_compression (s : A) :
    G.baseCompression A (s : P) = G.baseRepresentation A s :=
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetryRepeatedInclusion line 88
Source documentation
The actual base symmetry determines all normalized repeated-letter inclusions required by the word multiplicities.
```
def baseSymmetryRepeatedInclusion (s : A) (hzero : G.trace (s : P) = 0)
    (hself : star s = s) (hsquare : s * s = 1) (htrace : G.trace 1 = 1) (k : ℕ) :
    G.baseSpace A →ₗᵢ[ℂ] WordMultiplicity (G.baseVector A 1) k :=
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity