MATHLIBANNEX / CANONICAL DECLARATION CARD

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 .

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.

Proof steps

  1. Use the local exact-transport theorem for to fix and . These choices do not depend on , , or the later approximation request.

  2. Approximate every element of in a common stage within , and pass to . Purification gives a unit vector whose vector state agrees with on stage . Compatibility of the inclusions gives agreement on the earlier stage as well.

  3. The assumed entrywise tests for are therefore the tests for in . Exact local transport supplies and with and the required all-time protection.

  4. For and a stage approximant , the two vector states agree at . Each has norm at most , so their difference at is bounded by .

Main citations

Lean source signature (exact)

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'

Here rho is the fixed representation , sigma is the later representation, and F is protected throughout p. The primed variables F' and epsilon' specify the later endpoint approximation. Representation.vectorFunctional rho (rho u xi) is the state after transport; the theorem compares it with the state of eta under sigma.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 7711b3c3062f35d4f40941c530616797fcdd6ff68d6df057976f2c34a611097c

Exposition revision: 1 · SHA-256: 5c025351e5f794d88c7ae8ae8475b719da90a5ba389646a4db41b2537c5b2974

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: f78dd62ab2e788f74a4de2bbc109b6fe31cac02d5a22fd2bc3e461654168cef6

Back to top ↑