TracialCornerHilbert.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The normalized tracial Hilbert representation of an actual C-star corner. Its density and action are inherited from the ambient tracial representation.

def OAI.KadisonSimilarity.TracialCornerGeometry.cornerAlgebraVector line 20
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerAlgebraVector_coe line 27
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerAlgebraVector_dense line 30
def OAI.KadisonSimilarity.TracialCornerGeometry.normalizedCornerVector line 39
Source documentation
Rescale the ordinary corner vectors so that their inner product is the normalized corner trace.
```
def normalizedCornerVector (c : ℂ) : CStarCorner p hp →ₗ[ℂ] G.corner p p :=
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.TracialCornerGeometry.normalizedCornerVector_coe line 42
theorem OAI.KadisonSimilarity.TracialCornerGeometry.normalizedCornerVector_dense line 45
def OAI.KadisonSimilarity.TracialCornerGeometry.cornerGeometry line 52
Source documentation
The corner representation is constructed without a new GNS or free-product existence assumption. Only the scalar normalization is chosen.
```
def cornerGeometry (c : ℂ) (hc : c ≠ 0) (hcτ : star c * c = (G.trace p)⁻¹) :
    TracialCornerGeometry (CStarCorner p hp) (G.corner p p) where
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerGeometry_vector_injective line 70
theorem OAI.KadisonSimilarity.TracialCornerGeometry.cornerNormalization_ne_zero line 81
Source documentation
The positive trace supplies the concrete inverse-square-root scalar.
```
theorem cornerNormalization_ne_zero {t : ℝ} (ht : 0 < t) :
    dihedralNormalization t ≠ 0 := by
…
```
Mentions: OAI.KadisonSimilarity.dihedralNormalization
def OAI.KadisonSimilarity.TracialCornerGeometry.normalizedCornerGeometry line 90
Source documentation
The normalized tracial representation on pL²(P)p, with the scalar chosen from the actual trace of p.
```
def normalizedCornerGeometry {t : ℝ} (ht : 0 < t) (htp : G.trace p = (t : ℂ)) :
    TracialCornerGeometry (CStarCorner p hp) (G.corner p p) :=
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.TracialCornerGeometry.normalizedCornerGeometry_trace_one line 95
theorem OAI.KadisonSimilarity.TracialCornerGeometry.normalizedCornerGeometry_vector_injective line 101