MATHLIBANNEX / CANONICAL DECLARATION CARD

Transported flags vanish on vectors generated by a trace vector

MathlibAnnex.CStarAlgebra.CAR.tendsto_transportedFlag_orbit_zero

theorem

Turns decay of projection traces into norm convergence on each source-orbit vector.

Statement

Let be a unital star representation of the completed CAR algebra on a complete complex Hilbert space. Suppose implements the normalized trace from the CAR trace construction: for all . For the transported projections of a fixed shell family and every , one has in norm as .

Assumptions

Let be the completed CAR algebra with matrix stages embedded by . Write for the image of the first diagonal matrix unit, , and for the root state characterized by on each stage, where is its canonical embedding.

Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes , with root index and representative states .

A fixed shell family consists of complex-linear unital star automorphisms and elements satisfying , and .

At the root, is the identity and . Set .

The space lies in an arbitrary universe; it need not be separable. The vector-functional equality is assumed for every . Cyclicity of in all of is not assumed, nor is irreducibility of . Inner products are linear in their second argument. Here is the algebra of bounded complex-linear operators on .

Conclusion

Each fixed vector is sent to zero in the limit. The estimate proves this directly.

Proof route

For a projection , the vector-functional hypothesis gives . Traciality rewrites this as . Since , positivity gives the bound . Apply it to , whose trace is by the transported-flag trace theorem, and let tend to infinity.

Proof steps

  1. Use and star preservation to express the squared norm as .

  2. Use the trace identity and the positive order bound on to obtain .

  3. Insert the exact value . The nonnegative squared norms are squeezed to zero, which implies norm convergence of the vectors.

Main citations

Lean source signature (exact)

theorem tendsto_transportedFlag_orbit_zero (family : RepresentativeShellFamily)
    (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit)
    (σ : Representation Limit H) (ξ : H)
    (hξ : ∀ a, Representation.vectorFunctional σ ξ a = trace a) (b : Limit) :
    Tendsto (fun n ↦ σ (transportedFlag family i n) (σ b ξ)) atTop (nhds 0)

Here Limit is , trace is , and transportedFlag family i n is . The source index i is the index used here. The source letter H denotes the comparison space called above. vectorFunctional σ ξ a is . The filter expression asserts that tends in norm to zero as , for each fixed ; it makes no additional cyclicity assertion.

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

Lean realization notes

This declaration is a statement about orbit vectors and norm convergence of their images. It does not claim operator-norm convergence of the projections, or convergence on every vector of an arbitrary ambient representation without an additional argument.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:f96955493b7d58c74b287570a9cb14f2c543dd94a8fb260bd3afdd4344070a5f

Card revision: 1 · SHA-256: 1564975d5834ba5bc32bb5e411e16146fa3982ecafaac55210b5dbee2faeab6a

Exposition revision: 1 · SHA-256: a452e4aab867448a162caa4176581bc5f86e2f1a97100278e52380108f7b6a8e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: c3d081f7bedf0ebd8d683b6cae72e57293712695c2cb02f8738da0c3dd814041

Back to top ↑