TraceHilbertActions.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Bimodule actions on the trace Hilbert space

The canonical completion carries left and right multiplication. Its unitary actions give the bounded-ball estimate.

def OAI.KadisonKastler.concreteTraceLeftAction line 20
Source documentation
Left multiplication in the canonical trace representation.
```
def concreteTraceLeftAction (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    Algebra M →⋆ₐ[ℂ] (ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM) :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert
def OAI.KadisonKastler.concreteTraceRightAction line 26
Source documentation
Right multiplication in the canonical trace representation.
```
def concreteTraceRightAction (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (a : Algebra M) : ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert
theorem OAI.KadisonKastler.concreteTraceLeftAction_embedding line 31
theorem OAI.KadisonKastler.concreteTraceRightAction_embedding line 38
def OAI.KadisonKastler.concreteTraceLeftUnitary line 52
Source documentation
Left multiplication by a unitary is a unitary on the completion.
```
def concreteTraceLeftUnitary (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (u : unitary (Algebra M)) :
    unitary (ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM) :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert
theorem OAI.KadisonKastler.concreteTraceRightUnitary_norm line 57
theorem OAI.KadisonKastler.concreteTraceRightUnitary_inverse line 67
def OAI.KadisonKastler.concreteTraceRightUnitary line 80
Source documentation
Right multiplication by a unitary is a unitary on the completion.
```
def concreteTraceRightUnitary (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (u : unitary (Algebra M)) :
    unitary (ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM) :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert
theorem OAI.KadisonKastler.concreteTraceLeftUnitary_coe line 94
theorem OAI.KadisonKastler.concreteTraceRightUnitary_coe line 100

theorem OAI.KadisonKastler.concreteTrace_bimodular_bound line 108

Source documentation

The bounded-ball estimate on the constructed canonical Hilbert space, with actual multiplication actions and no action-existence hypothesis.

theorem concreteTrace_bimodular_bound
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    {R : Type*} [CStarAlgebra R] (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (V : ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM)
    (hVL : ∀ u : unitary R, Commute V (concreteTraceLeftAction hM (φ u)))
    (hVR : ∀ u : unitary R, Commute V (concreteTraceRightAction hM (φ u)))
    {K : ℝ} (hK : ∀ x y : Algebra M, ‖x‖ ≤ 1 → ‖y‖ ≤ 1 →
      ‖inner ℂ (V (concreteTraceEmbedding hM x)) (concreteTraceEmbedding hM y)‖ ≤ K) :
    ‖V‖ ≤ 384 * K := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert, OAI.KadisonKastler.concreteTraceLeftAction, OAI.KadisonKastler.concreteTraceRightAction, OAI.KadisonKastler.concreteTraceEmbedding