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.
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.
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
Use and star preservation to express the squared norm as .
Use the trace identity and the positive order bound on to obtain .
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)| In the source | Mathematical meaning |
|---|---|
family; i : GNSClass Limit |
The given shell family and fixed class
(i in the source), supplying
at every natural stage. |
σ : Representation Limit H; ξ : H |
The unital star representation
on the complete complex Hilbert space denoted H in the
source, and a vector
.
Neither irreducibility nor cyclicity in all of
is assumed. |
hξ : ∀ a, Representation.vectorFunctional σ ξ a = trace a |
For every , , with inner product linear in the second entry. This is the trace-vector hypothesis on the given . |
b : Limit; σ b ξ |
A fixed element and the orbit vector . |
fun n ↦ σ (transportedFlag family i n) (σ b ξ) |
The vector sequence : the projection acts on the fixed orbit vector, not on in the algebra. |
Tendsto (...) atTop (nhds 0) |
As the natural number , this sequence tends to the zero vector in the norm topology of . This conclusion is for each fixed ; it does not assert operator-norm convergence or convergence on every vector of an arbitrary ambient . |
Further source notes: 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 · Back to Project
Exact content identity
Declaration: MathlibAnnex.CStarAlgebra.CAR.tendsto_transportedFlag_orbit_zero
Accepted content SHA-256: 9138d3fdb637a34fee071ec248a373a229c141eb0f2172e319227577e624e79d
Accepted source guide SHA-256: d6f97e5f24fe34a45010f6305af83d461b52365ddb73c8161276f444fe1890f4
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73