OAI/Analysis/OperatorAlgebra/ExpectationHypertrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite part of the injectivity argument starts with a hypertrace. Composing a tracial state with the actual cpc expectation gives that hypertrace, since the multiplicative-domain calculation is bimodular.

  1. theorem OAI.WeakPureInfiniteness.expectation_hypertrace line 18