MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

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 .

Proof steps

  1. For , choose with , using density of the stages.

  2. For , the exact finite-stage compression identity gives .

  3. Linearity gives . Hence .

  4. This bound holds for every , which is the required norm limit.

Main citations

Lean source signature (exact)

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

Here Limit is , rootState is , rootFlag n is , and compressionError n x is . The filter expression says that this real-valued sequence of norms tends to as .

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:5d44ee0aca9e46791d96b1f135b1092607d2b62670313827b2f813e5fe6e9be3

Card revision: 1 · SHA-256: c2ac9201baafd4343fd842fed3bb480153e0b78995eb4dce3491d6475fdb9b00

Exposition revision: 1 · SHA-256: 4119ae48aa3d3cc4f60c5e5adbe7f4530c6ff48f027809564ab08eb487d7cb30

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 80678107836d77972acbfed5b188f0c57a3a9a6511151dbb16b7a02d2b4e5420

Back to top ↑