UltrapowerGeneratedTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The two compressions used in the finite-factor argument are combined here. The resulting operator on the generated algebra retains commutation, all prescribed small-corner bounds, and the original commutator norm.

def OAI.KadisonSimilarity.generatedUltrapowerOperator line 45
Source documentation
The concrete operator after Hilbert-ultrapower and generated-algebra compression. No operator on the generated algebra is chosen independently.
```
def generatedUltrapowerOperator (T : τB.GNS →L[ℂ] τB.GNS) :
    (restrictedPositiveTrace τQ L).GNS →L[ℂ] (restrictedPositiveTrace τQ L).GNS :=
…
```
Mentions: OAI.KadisonSimilarity.restrictedPositiveTrace
theorem OAI.KadisonSimilarity.generatedUltrapowerOperator_commutes line 49
theorem OAI.KadisonSimilarity.generatedUltrapowerOperator_traceCornerBound line 62

theorem OAI.KadisonSimilarity.norm_commutator_le_generatedUltrapowerOperator line 77

Source documentation

A bound from the free-corner theorem on this generated algebra controls the original operator on its original GNS space, with the identical constant.

theorem norm_commutator_le_generatedUltrapowerOperator
    (hconst : ∀ b, constant τB hB ω trB b ∈ L)
    (T : τB.GNS →L[ℂ] τB.GNS) (b : B) :
    ‖commutator T (τB.gnsStarAlgHom b)‖ ≤
      ‖(gnsTracialGeometry (restrictedPositiveTrace τQ L)
          (restrictedPositiveTrace_tracial τQ L (quotientTrace_tracial τB hB ω trB))).baseOperator
        ((constant τB hB ω trB).codRestrict L hconst).range
        (commutator (generatedUltrapowerOperator τB hB ω trB L T)
          ((restrictedPositiveTrace τQ L).gnsStarAlgHom
            ((constant τB hB ω trB).codRestrict L hconst b)))‖ :=
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.gnsTracialGeometry, OAI.KadisonSimilarity.restrictedPositiveTrace, OAI.KadisonSimilarity.restrictedPositiveTrace_tracial, OAI.KadisonSimilarity.generatedUltrapowerOperator