Root compression becomes scalar in norm

MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_compressionError

theorem

Extends an exact rank-one compression identity on finite stages to a pointwise norm limit on the completed algebra.

Statement

Let be the completed CAR algebra with stage maps and root state . Put , where is the projection onto the first coordinate. Then, for every fixed , as .

Assumptions

The stages are linked by , and is their norm completion. The functional is the continuous root state. Each is a self-adjoint projection of norm at most one. The element is arbitrary but fixed while tends to infinity.

Conclusion

Writing , the theorem gives for every . The error is an element of ; its norm is the real-valued quantity that converges.

This is pointwise convergence in , not convergence in operator norm uniformly over the unit ball. It also does not assert norm convergence of the projections . The displayed projections have rank one at their defining finite stage; no rank-one assertion in an arbitrary representation of is used.

Proof route

If lies in a finite stage, rank-one compression gives whenever . For arbitrary , the projection norm bound and boundedness of give , uniformly in . Approximate the fixed by such a , and apply this estimate to .

theorem tendsto_norm_compressionError (x : Limit) :
    Filter.Tendsto (fun n => ‖compressionError n x‖) Filter.atTop (nhds 0)

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

Earlier published Card and PDF