TracialUltrapowerConstants.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Both ultrapower constructions preserve the original constant Hilbert space exactly. Compression back to that space recovers the original operator.

theorem OAI.KadisonSimilarity.compression_through_composite line 15
def OAI.KadisonSimilarity.constantTracialGNSInclusion line 30
Source documentation
The trace-preserving constant inclusion gives the actual GNS inclusion.
```
def constantTracialGNSInclusion : τ.GNS →ₗᵢ[ℂ] (quotientTrace τ h1 ω htr).GNS :=
…
```
theorem OAI.KadisonSimilarity.tracialUltrapower_constant_inclusion line 36
Source documentation
Going through the tracial quotient agrees with the constant Hilbert ultrapower inclusion on the entire completed Hilbert space.
```
theorem tracialUltrapower_constant_inclusion :
    (tracialUltrapowerGNSInclusion τ h1 ω htr).toContinuousLinearMap.comp
      (constantTracialGNSInclusion τ h1 ω htr).toContinuousLinearMap =
      (constantHilbertInclusion (H := τ.GNS) ω).toContinuousLinearMap := by
…
```
Mentions: OAI.KadisonSimilarity.tracialUltrapowerGNSInclusion, OAI.KadisonSimilarity.constantTracialGNSInclusion, OAI.KadisonSimilarity.constantHilbertInclusion
theorem OAI.KadisonSimilarity.constant_compression_tracialUltrapower line 63
Source documentation
The compressed ultrapower operator agrees with the original operator after compression to the constant tracial subspace.
```
theorem constant_compression_tracialUltrapower (T : τ.GNS →L[ℂ] τ.GNS) :
    (constantTracialGNSInclusion τ h1 ω htr).toContinuousLinearMap.adjoint.comp
      ((tracialUltrapowerCompression τ h1 ω htr T).comp
        (constantTracialGNSInclusion τ h1 ω htr).toContinuousLinearMap) = T := by
…
```
Mentions: OAI.KadisonSimilarity.constantTracialGNSInclusion, OAI.KadisonSimilarity.tracialUltrapowerCompression