TracialUltrapowerActions.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded left-multiplier sequences reduce the tracial GNS subspace of the Hilbert ultrapower. The compressed operator therefore inherits every eventual coordinate commutator estimate.

def OAI.KadisonSimilarity.gnsLeftSequence line 20
Source documentation
The actual uniformly bounded family of left multipliers.
```
def gnsLeftSequence (x : ℕ →ᵇ A) : lp (fun _ : ℕ => τ.GNS →L[ℂ] τ.GNS) ∞ :=
…
```
theorem OAI.KadisonSimilarity.gnsLeftSequence_apply line 26
theorem OAI.KadisonSimilarity.gnsLeftSequence_star line 29
theorem OAI.KadisonSimilarity.gnsLeftSequence_vector line 35

theorem OAI.KadisonSimilarity.tracialUltrapowerGNSInclusion_intertwines line 50

Source documentation

The inclusion intertwines the quotient's left action and the coordinate action.

theorem tracialUltrapowerGNSInclusion_intertwines (x : ℕ →ᵇ A) :
    (HilbertUltraproduct.map ω (gnsLeftSequence τ x)).comp
      (tracialUltrapowerGNSInclusion τ h1 ω htr).toContinuousLinearMap =
    (tracialUltrapowerGNSInclusion τ h1 ω htr).toContinuousLinearMap.comp
      ((quotientTrace τ h1 ω htr).gnsStarAlgHom (quotientHom τ h1 ω htr x)) := by
…

Mentions: OAI.KadisonSimilarity.gnsLeftSequence, OAI.KadisonSimilarity.tracialUltrapowerGNSInclusion

def OAI.KadisonSimilarity.tracialUltrapowerCompression line 71
Source documentation
Compression of the constant Hilbert-ultrapower operator to the tracial quotient's GNS space. No invariance of the original operator is needed.
```
def tracialUltrapowerCompression (T : τ.GNS →L[ℂ] τ.GNS) :
    (quotientTrace τ h1 ω htr).GNS →L[ℂ] (quotientTrace τ h1 ω htr).GNS :=
…
```

theorem OAI.KadisonSimilarity.norm_tracialUltrapowerCompression_commutator_le line 78

Source documentation

Eventual coordinate bounds survive the two constructions exactly.

theorem norm_tracialUltrapowerCompression_commutator_le
    (T : τ.GNS →L[ℂ] τ.GNS) (x : ℕ →ᵇ A) {c : ℝ} (hc : 0 ≤ c)
    (hbound : ∀ᶠ i in (ω : Filter ℕ), ‖commutator T (τ.gnsStarAlgHom (x i))‖ ≤ c) :
    ‖commutator (tracialUltrapowerCompression τ h1 ω htr T)
      ((quotientTrace τ h1 ω htr).gnsStarAlgHom (quotientHom τ h1 ω htr x))‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.tracialUltrapowerCompression