OAI/Analysis/OperatorAlgebra/TracialSpatialUnitaryState.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The spatial diagonal state in the finite tracial injectivity argument. The finite-vector argument follows Anantharaman--Delaroche, Pacific J. Math. 171 (1995), Lemma 3.7 and Proposition 3.6, pp. 328--330.

  1. theorem OAI.WeakPureInfiniteness.expectation_tracial_spatial_unitary_state line 17