TracialProductApproximation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Product-state approximation from the finite tracial vector construction.

lemma OAI.WeakPureInfiniteness.tracial_product_error_lt line 15

theorem OAI.WeakPureInfiniteness.expectation_spatial_product_approximation line 47

Source documentation

A finite family of diagonal trace coefficients is approximated by coefficients of the genuine spatial left/right representation.

theorem expectation_spatial_product_approximation (M : VonNeumannAlgebra H)
    [PartialOrder M.toStarSubalgebra] [StarOrderedRing M.toStarSubalgebra]
    (τ : Pureness.TracialState M.toStarSubalgebra)
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hE : CompletelyPositive E) (hEr : ∀ T, E T ∈ M)
    (hEf : ∀ T, T ∈ M → E T = T)
    (a : I → M.toStarSubalgebra) (u : I → unitary M.toStarSubalgebra)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ z : NuclearUltrapower.HilbertSchmidt H, ‖z‖ = 1 ∧
      0 ≤ NuclearUltrapower.hsOperator z ∧
      (∃ F : Submodule ℂ H, FiniteDimensional ℂ F ∧
        ∀ y, NuclearUltrapower.hsOperator z y ∈ F) ∧
…

Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.NuclearUltrapower.HilbertSchmidt, OAI.NuclearUltrapower.hsOperator