WeakClosure.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

The weak closure of the trace representation

Finite trace vectors define positive functionals on the GNS weak closure. Their supremum is additive, homogeneous, lower semicontinuous, and agrees with the original trace on its finite ideal.

This is the trace representation construction in The trace cone classifies Razak–Jacelon stabilizations.

def OAI.TraceConeClassification.ExtendedTrace.traceWeakClosure line 34
Source documentation
The weak-operator closed star algebra of the square-integrable representation.
```
def traceWeakClosure := weakClosure (NonUnitalStarAlgHom.range τ.traceGNSRep)
```
Mentions: OAI.TraceConeClassification.weakClosure
instance OAI.TraceConeClassification.ExtendedTrace.traceWeakClosure_closed line 35
instance OAI.TraceConeClassification.ExtendedTrace.traceWeakClosure_starOrdered line 38
lemma OAI.TraceConeClassification.ExtendedTrace.traceGNSRep_mem_weakClosure line 57
def OAI.TraceConeClassification.ExtendedTrace.traceGNSPositive line 62
Source documentation
The represented image of a positive element in the GNS weak closure.
```
def traceGNSPositive (a : Positive A) : Positive τ.traceWeakClosure :=
…
```
Mentions: OAI.TraceConeClassification.Positive
def OAI.TraceConeClassification.ExtendedTrace.IsNormalTrace line 67
Source documentation
Normality is preservation of every existing directed positive supremum.
```
def IsNormalTrace (w : ExtendedTrace τ.traceWeakClosure) : Prop :=
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
def OAI.TraceConeClassification.ExtendedTrace.IsSemifiniteTrace line 72
Source documentation
The usual semifiniteness condition, including boundary value infinity.
```
def IsSemifiniteTrace (w : ExtendedTrace τ.traceWeakClosure) : Prop :=
…
```
Mentions: OAI.TraceConeClassification.ExtendedTrace
lemma OAI.TraceConeClassification.ExtendedTrace.positive_starMul_sqrt line 85
def OAI.TraceConeClassification.ExtendedTrace.finiteTraceSqrt line 90
def OAI.TraceConeClassification.ExtendedTrace.traceVector line 95
lemma OAI.TraceConeClassification.ExtendedTrace.traceVector_norm_sq line 98
def OAI.TraceConeClassification.ExtendedTrace.traceVectorForm line 105
Source documentation
A finite-trace positive element defines a vector functional.
```
def traceVectorForm (a : Positive A) (ha : τ a < ∞)
    (T : τ.TraceGNS →L[ℂ] τ.TraceGNS) : ℝ :=
…
```
Mentions: OAI.TraceConeClassification.Positive
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_wot_continuous line 109
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_starMul line 115
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_rep_starMul line 120
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_nonneg line 133
abbrev OAI.TraceConeClassification.ExtendedTrace.FiniteTraceContraction line 150
Source documentation
Finite-weight positive strict contractions, with their operator order.
```
abbrev FiniteTraceContraction := {a : Positive A // τ a < ∞ ∧ ‖a.1‖ < 1}
```
Mentions: OAI.TraceConeClassification.Positive
lemma OAI.TraceConeClassification.ExtendedTrace.finite_cfc_nnreal line 152
lemma OAI.TraceConeClassification.ExtendedTrace.finiteTraceContraction_directed line 165
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_mono line 234
def OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight line 282
Source documentation
The supremum of the finite-vector functionals over finite-trace strict contractions.
```
def traceNormalWeight (T : Positive τ.traceWeakClosure) : ℝ≥0∞ :=
…
```
Mentions: OAI.TraceConeClassification.Positive
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_add line 285
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_smul line 290
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_zero line 295
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_add line 298
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_scale line 313
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_positive_continuous line 323
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_lowerSemicontinuous line 331
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_mono line 335
lemma OAI.TraceConeClassification.ExtendedTrace.traceVectorForm_rep_positive line 356
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_rep_le line 365
def OAI.TraceConeClassification.ExtendedTrace.finiteResolvent line 384
Source documentation
A finite resolvent contraction. The strictly positive denominator is retained also at the endpoint zero of the nonunital spectrum.
```
def finiteResolvent (a : Positive A) (ha : τ a < ∞) (r : ℝ≥0) (hr : 0 < r) :
    τ.FiniteTraceContraction := by
…
```
Mentions: OAI.TraceConeClassification.Positive
lemma OAI.TraceConeClassification.ExtendedTrace.finiteResolvent_val line 401
lemma OAI.TraceConeClassification.ExtendedTrace.finiteResolvent_conjugate line 404
lemma OAI.TraceConeClassification.ExtendedTrace.finiteResolvent_residual_norm line 420
lemma OAI.TraceConeClassification.ExtendedTrace.finiteResolvent_conjugate_tendsto line 451
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_rep_eq_of_finite line 460
lemma OAI.TraceConeClassification.ExtendedTrace.traceNormalWeight_rep_eq line 471