TracialCornerExpectations.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Restricting a tracial expectation to a corner. The normalized corner trace and the restricted expectation are constructed from the ambient ones.

def OAI.KadisonSimilarity.CStarCorner.subalgebra line 19
Source documentation
The part of an ambient unital star algebra lying in the corner.
```
def subalgebra (A : StarSubalgebra ℂ P) (hpA : p ∈ A) :
    StarSubalgebra ℂ (CStarCorner p hp) where
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.CStarCorner.mem_subalgebra line 40
def OAI.KadisonSimilarity.CStarCorner.normalizedTrace line 44
Source documentation
Normalize the ambient trace by the trace of the corner identity.
```
def normalizedTrace (τ : P →ₗ[ℂ] ℂ) : CStarCorner p hp →ₗ[ℂ] ℂ where
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.CStarCorner.normalizedTrace_apply line 52
theorem OAI.KadisonSimilarity.CStarCorner.normalizedTrace_one line 55
theorem OAI.KadisonSimilarity.CStarCorner.normalizedTrace_tracial line 59
theorem OAI.KadisonSimilarity.CStarCorner.normalizedTrace_faithful line 65
theorem OAI.KadisonSimilarity.TracialExpectation.map_mem_corner line 86
Source documentation
Bimodularity makes the ambient expectation preserve the corner.
```
theorem map_mem_corner (x : CStarCorner p hp) :
    E.map (x : P) ∈ cstarCornerSubalgebra p hp := by
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.cstarCornerSubalgebra
def OAI.KadisonSimilarity.TracialExpectation.corner line 93
Source documentation
The restriction is trace preserving for the normalized corner trace.
```
def corner : TracialExpectation (CStarCorner.normalizedTrace p hp τ)
    (CStarCorner.subalgebra p hp C hpC) where
…
```
Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.CStarCorner.normalizedTrace, OAI.KadisonSimilarity.CStarCorner.subalgebra
theorem OAI.KadisonSimilarity.TracialExpectation.corner_map_coe line 105

theorem OAI.KadisonSimilarity.TracialExpectation.free_corner_compression line 111

Source documentation

The ambient expectation formula used in the dihedral corner follows from freeness in the normalized corner, rather than being extra data.

theorem free_corner_compression (ht : τ p ≠ 0)
    (D : StarSubalgebra ℂ P) (hpD : p ∈ D)
    (hfree : ScalarFree (CStarCorner.normalizedTrace p hp τ)
      (CStarCorner.subalgebra p hp D hpD) (CStarCorner.subalgebra p hp C hpC))
    (e b : CStarCorner p hp) (he : (e : P) ∈ D) (hb : (b : P) ∈ C)
    (hb0 : τ (b : P) = 0) :
    E.map ((e : P) * (b : P) * (e : P)) =
      ((τ p)⁻¹ * τ (e : P)) ^ 2 • (b : P) := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CStarCorner.normalizedTrace, OAI.KadisonSimilarity.CStarCorner.subalgebra, OAI.KadisonSimilarity.CStarCorner