ConcreteTraceHilbert.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The canonical separable trace Hilbert realization

The trace completion provides the Hilbert-space norm estimates used by boundary comparison.

theorem OAI.KadisonKastler.traceHilbert_factor line 22
theorem OAI.KadisonKastler.traceHilbert_nonzero line 28
abbrev OAI.KadisonKastler.ConcreteTraceHilbert line 34
Source documentation
The completion of the algebra in its canonical trace inner product.
```
abbrev ConcreteTraceHilbert (hM : Generator.IsII1Factor M.toStarSubalgebra) :=
…
```
Mentions: OAI.Generator.IsII1Factor
def OAI.KadisonKastler.concreteTraceEmbedding line 39
Source documentation
The algebraic inclusion into its actual trace Hilbert completion.
```
def concreteTraceEmbedding (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    Algebra M →ₗ[ℂ] ConcreteTraceHilbert hM :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert
theorem OAI.KadisonKastler.concreteTraceEmbedding_norm line 46
theorem OAI.KadisonKastler.concreteTraceEmbedding_denseRange line 63
theorem OAI.KadisonKastler.separableSpace_of_traceHilbert line 77
Source documentation
Trace separability of the algebra makes any dense faithful trace Hilbert realization separable.
```
theorem separableSpace_of_traceHilbert {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] {τ : FaithfulTracialState (Algebra M)}
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hsep : TraceSeparable τ Set.univ) (hdense : DenseRange J) : SeparableSpace E := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.TraceSeparable
instance OAI.KadisonKastler.concreteTraceHilbert_separable line 97
Source documentation
The trace Hilbert space of a separably acting II₁ factor is separable.
```
instance concreteTraceHilbert_separable [SeparableSpace H]
    (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    SeparableSpace (ConcreteTraceHilbert hM) :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.ConcreteTraceHilbert