NormalWeight.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The tracial weight on the GNS weak closure

Finite-root actions recover the Hilbert norm. Strong-star density then extends the trace identity from the represented algebra to its weak closure.

def OAI.TraceConeClassification.ExtendedTrace.finiteRootAction line 24
Source documentation
The positive contractive action of a finite trace square root.
```
def finiteRootAction (e : τ.FiniteTraceContraction) : τ.TraceGNS →L[ℂ] τ.TraceGNS :=
…
```
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_norm_le line 27
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_apply_norm_le line 33
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_on_lambda line 37
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_iSup_lambda line 51
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_detects_norm line 60
Source documentation
The finite-root actions detect the Hilbert norm by density and the finite trace identity.
```
lemma finiteRootAction_detects_norm (ξ : τ.TraceGNS) (r : ℝ) (hr : 0 ≤ r)
    (h : ∀ e : τ.FiniteTraceContraction, ‖τ.finiteRootAction e ξ‖ ≤ r) : ‖ξ‖ ≤ r := by
…
```
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_iSup_norm line 84
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_double_rep line 117
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_double line 132
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_tracial line 156
def OAI.TraceConeClassification.ExtendedTrace.normalTraceCandidate line 179
Source documentation
The tracial weight on the GNS weak operator closure.
```
def normalTraceCandidate : ExtendedTrace τ.traceWeakClosure where
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace