The normalized trace on a finite CAR stage

MathlibAnnex.CStarAlgebra.CAR.stageTrace

def

The normalized matrix trace provides a positive tracial functional compatible with the CAR inclusions.

Statement

For , let with its operator norm. The finite-stage trace is the continuous complex-linear functional whose value is . The factor makes .

Definition

Take the normalized diagonal sum as a linear map. Each diagonal entry satisfies , so the triangle inequality gives . This bound supplies continuity. Positivity follows by expanding the diagonal of into sums of squared absolute values; the trace identity follows by interchanging the two finite summations. Amplification repeats every diagonal entry twice, exactly cancelling the change in normalization.

Assumptions

The index may be zero, in which case . No representation, choice of vector, or limiting operation enters this definition.

Conclusion

The functional is bounded by , is positive on , and satisfies . Under the standard CAR inclusion , given by and coordinate reindexing, . These are the separately proved properties cited below.

The root projection has trace ; the root-coordinate functional instead takes value there. Thus the trace and the product-vector functional serve different purposes. The declaration here defines a finite-stage functional, not a new assertion about a trace on the completion.

noncomputable def stageTrace (n : ℕ) : Stage n →L[ℂ] ℂ :=
  (stageTraceLinear n).mkContinuous 1 fun a ↦ by
    simpa only [one_mul] using norm_stageTraceLinear_le n a

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF