TracialSubalgebraTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Restriction to the closed algebra generated by the free factors preserves both commutation and the small-corner estimate.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseOperator_commutator_norm_le line 20
Source documentation
Compression to the actual base Hilbert subspace preserves any commutator bound against an element of the base algebra.
```
theorem baseOperator_commutator_norm_le (T : H →L[ℂ] H) (a : L)
    {c : ℝ} (hc : ‖commutator T (G.left (a : P))‖ ≤ c) :
    ‖commutator (G.baseOperator L T) (G.baseRepresentation L a)‖ ≤ c := by
…
```
Mentions: OAI.KadisonSimilarity.commutator
def OAI.KadisonSimilarity.TracialCornerGeometry.cornerInclusion line 33
Source documentation
A corner element of a subalgebra is the same ambient corner element, with exactly the same norm.
```
def cornerInclusion (e : L) (he : IsStarProjection e)
    (x : CStarCorner e he) : CStarCorner (e : P) (he.map L.subtype) :=
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_traceCornerBound line 40
Source documentation
The small-corner hypothesis survives restriction to the closed generated algebra, without invariance of the operator being compressed.
```
theorem baseGeometry_traceCornerBound (D : StarSubalgebra ℂ P)
    (T : H →L[ℂ] H) {t ε : ℝ} (hbound : G.TraceCornerBound D T t ε) :
    (G.baseGeometry L).TraceCornerBound (D.comap L.subtype) (G.baseOperator L T) t ε := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.TraceCornerBound

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseGeometry_commutes line 48

Source documentation

Commutation with the other factor also survives the same compression.

theorem baseGeometry_commutes (D : StarSubalgebra ℂ P)
    (T : H →L[ℂ] H)
    (hcomm : ∀ a : D, T.comp (G.left (a : P)) = (G.left (a : P)).comp T) :
    ∀ a : D.comap L.subtype,
      (G.baseOperator L T).comp ((G.baseGeometry L).left (a : L)) =
        ((G.baseGeometry L).left (a : L)).comp (G.baseOperator L T) := by
…