MATHLIBANNEX / CANONICAL DECLARATION CARD

Approximating another vector state along a unitary path

MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx

theorem

A fixed irreducible CAR representation can approximate any vector state on finitely many elements by moving a given unit vector.

Statement

Let be the completed CAR algebra: the norm completion of the increasing union of under the unital embeddings (with the fixed coordinate reindexing). Write for the canonical isometric inclusion and for its matrix units. A representation is a unital complex star homomorphism into the bounded operators on a complex Hilbert space. Irreducibility means nonzero action and no proper nonzero closed reducing subspace. We use the inner product conjugate linear in its first argument and write for the vector functional. Let be irreducible with , let be any representation, and choose unit vectors and . For every finite and , there exist a unitary and a norm-continuous path from to such that for all .

Assumptions

The spaces and are complete complex Hilbert spaces. Both representations are unital; only must be irreducible. There are no initial stage-state tests and no protected finite set.

Conclusion

The approximating state is obtained from the specified starting vector by a unitary in the identity path component of . The approximation is on the prescribed finite set at the endpoint.

Proof route

Keep the given vectors and fixed. Purification supplies a new unit vector that realizes the target state on a sufficiently large stage . To move to , use the fixed-stage transport lemma at stage , where its tests are automatic. These are two different stages: controls approximation, whereas stage supplies transport without any near-centrality requirement.

Proof steps

  1. Choose so that each has an approximant with . Apply finite-stage purification to the given , , and at stage . Its hypotheses hold because is nonzero and irreducible, both representations are unital, and . It gives with and for all . This is a new vector; the prescribed starting vector is not replaced.

  2. Use the fixed-stage exact-transport lemma, not the protected-finite-set theorem. For a prescribed stage and a positive commutator tolerance, it supplies a before the pair of unit vectors is chosen. Its hypothesis compares their vector functionals on the matrix units of that stage. Set and take the auxiliary commutator tolerance to be ; its commutator conclusion will not be needed.

  3. The inputs to this transport lemma are in the same representation , not and from different spaces. Since and , unitality and the two unit-vector norms give . This is the only matrix-unit test at stage . Thus the lemma supplies and a path from to with . No comparison between these states on the larger stage , and no norm closeness of and , is required.

  4. For each , the two states agree at and are contractive, so Substitute to obtain the asserted endpoint estimate.

Main citations

Lean source signature (exact)

theorem exists_unitary_crossRepresentation_path_approx
    {H K : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [Nontrivial H]
    [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
    (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)
    (sigma : Representation Limit K) (xi : H) (eta : K)
    (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1)
    (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ u : unitary Limit, ∃ p : Path 1 u, ∀ a ∈ F,
      ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a -
        Representation.vectorFunctional sigma eta a‖ < epsilon

Here rho is , sigma is , and xi, eta are the given unit vectors. Path 1 u is a continuous unitary path; the final bound is the endpoint estimate on F. In the linked proof, zeta is the new finite-stage realization of the state of eta; htrans xi zeta applies the fixed-stage lemma inside rho at stage zero. The signature imposes no initial comparison of the states of xi and eta.

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

Lean realization notes

The conclusion supplies a path but makes no near-centrality claim and no uniform approximation claim along that path. It does not identify the two representations or give exact equality of their states on all elements.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: ca7b92d9fb47c907d06289cd2500a60d26d2ae92daa125feae35b8795c8b1b18

Exposition revision: 1 · SHA-256: 9e5ffe2c1b5b2c5dd3b1441d8e6c427441f373797a66b5afffe55da44ec792ad

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: ba201ca41f9aeb157f79785a5da063918f166ac5bc80c8f075d32dc52347f404

Back to top ↑