SemifiniteWeight.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The faithful normal semifinite trace extension

The trace on the GNS weak closure is semifinite, faithful, and normal. The GNS space is separable for a separable algebra, and the representation is nondegenerate.

def OAI.TraceConeClassification.ExtendedTrace.finiteSubelement line 27
Source documentation
A finite-weight subelement of a positive operator in the GNS weak closure.
```
def finiteSubelement (T : Positive τ.traceWeakClosure) (e : τ.FiniteTraceContraction) :
    Positive τ.traceWeakClosure := Positive.conjugate (CFC.sqrt T.1) (τ.traceGNSPositive e.1)
```
Mentions: OAI.TraceConeClassification.Positive, OAI.TraceConeClassification.Positive.conjugate
lemma OAI.TraceConeClassification.ExtendedTrace.finiteSubelement_le line 30
lemma OAI.TraceConeClassification.ExtendedTrace.finiteSubelement_weight line 44
lemma OAI.TraceConeClassification.ExtendedTrace.normalTraceCandidate_semifinite line 71
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_nonneg line 98
lemma OAI.TraceConeClassification.ExtendedTrace.finiteRootAction_approximates line 101
lemma OAI.TraceConeClassification.ExtendedTrace.traceGNSLambda_star_norm line 117

lemma OAI.TraceConeClassification.ExtendedTrace.finiteTraceVector_cyclic_approx line 128

Source documentation

Right multiplication by finite roots approximates every algebraic GNS vector.

lemma finiteTraceVector_cyclic_approx (x : τ.finiteSquareAlgebra) (ε : ℝ) (hε : 0 < ε) :
    ∃ e : τ.FiniteTraceContraction,
      ‖τ.traceGNSLambda x-τ.traceGNSRep x.1 (τ.traceVector e.1 e.2.1)‖ < ε := by
…

lemma OAI.TraceConeClassification.ExtendedTrace.normalTraceCandidate_faithful line 151

lemma OAI.TraceConeClassification.ExtendedTrace.traceWeakClosure_lub_strong line 217

Source documentation

The order supremum in the weak closure is its strong monotone limit.

lemma traceWeakClosure_lub_strong (s : Set (Positive τ.traceWeakClosure))
    (hne : s.Nonempty) (hdir : DirectedOn (· ≤ ·) s)
    (a : Positive τ.traceWeakClosure) (hlub : IsLUB s a) :
    letI : Nonempty s := hne.to_subtype
…

Mentions: OAI.TraceConeClassification.Positive

lemma OAI.TraceConeClassification.ExtendedTrace.normalTraceCandidate_normal line 263
theorem OAI.TraceConeClassification.ExtendedTrace.trace_normal_extension line 291
Source documentation
The faithful normal semifinite extension of the trace to its GNS weak closure.
```
theorem trace_normal_extension (τ : ExtendedTrace A) :
    ∃ w : ExtendedTrace τ.traceWeakClosure,
      τ.IsNormalTrace w ∧ τ.IsSemifiniteTrace w ∧
      (∀ a, w a = 0 → a = Positive.zero) ∧
      (∀ a : Positive A, a.1 ∈ τ.finiteIdeal → w (τ.traceGNSPositive a) = τ a) := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace, OAI.TraceConeClassification.Positive.zero, OAI.TraceConeClassification.Positive
lemma OAI.TraceConeClassification.ExtendedTrace.finite_cyclic_root_dist line 308
lemma OAI.TraceConeClassification.ExtendedTrace.finite_cyclic_continuous line 322
theorem OAI.TraceConeClassification.ExtendedTrace.traceGNS_separable line 338
Source documentation
The GNS representation of an extended trace on a separable algebra is separably acting.
```
theorem traceGNS_separable [SeparableSpace A] (τ : ExtendedTrace A) :
    SeparableSpace τ.TraceGNS := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.ExtendedTrace.traceGNS_approximateUnit_strong line 381
lemma OAI.TraceConeClassification.ExtendedTrace.traceWeakClosure_one line 409
theorem OAI.TraceConeClassification.ExtendedTrace.traceGNS_vonNeumann line 426
Source documentation
The weak closure of the GNS representation is a von Neumann algebra.
```
theorem traceGNS_vonNeumann (τ : ExtendedTrace A) :
    ∃ N : VonNeumannAlgebra τ.TraceGNS,
      (N : Set (τ.TraceGNS →L[ℂ] τ.TraceGNS)) = τ.traceWeakClosure := by
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace