Cross-representation state approximation with a protected finite set

MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_crossRepresentation_path_approx

theorem

Finite entrywise tests allow new state approximation while an entire unitary path nearly fixes earlier data.

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. Fix an irreducible with . For every finite and , there exist and with the following property. Let be any representation and let , be unit vectors whose vector states differ by less than on every . For every later finite set and , there are and a norm-continuous path from to such that for every . Throughout the path, both conjugation errors on are less than .

Assumptions

The spaces and are complete complex Hilbert spaces. Only is required to be irreducible. The order of choices is essential: come first, then , then the second representation and the unit vectors satisfying the tests, and finally the new approximation requests .

Conclusion

Writing the all-time protection explicitly, and for every and . At the endpoint the transported vector state approximates the target on the independently specified later set .

The endpoint approximation does not assert equality of the two states on all of , unitary equivalence of the representations, or state approximation along every intermediate point of the path. The second representation need not be irreducible.

Proof route

Choose the tests using the exact local transport theorem in the first representation. Approximate the later set by a larger stage. Finite-stage purification realizes the second vector state exactly on that larger stage inside , so the original tests still hold. Exact local transport reaches this purified vector while protecting . Contractivity of unit vector states controls the approximation error on the later set.

theorem exists_stageTests_crossRepresentation_path_approx
    {H : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [Nontrivial H]
    (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)
    (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ n, ∃ delta > 0,
      ∀ {K : Type*}
        [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
        (sigma : Representation Limit K) (xi : H) (eta : K),
      ‖xi‖ = 1 → ‖eta‖ = 1 →
      (∀ i j : Fin (2 ^ n),
        ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) -
          Representation.vectorFunctional sigma eta (limitMatrixUnit n i j)‖ < delta) →
      ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' →
        ∃ u : unitary Limit,
          ∃ p : Path 1 u,
          (∀ t, ∀ a ∈ F,
            ‖(p t : Limit) * a * star (p t : Limit) - a‖ < epsilon ∧
            ‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon) ∧
          ∀ a ∈ F',
            ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a -
              Representation.vectorFunctional sigma eta a‖ < epsilon'

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

Earlier published Card and PDF