OAI/Analysis/FiniteFactor/CrossedProduct/TracialRepresentation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceTracialRepresentation line 11

   Source documentation

   Actual instantiation of the certified tracial-representation API. Both central obligations are proved for this source algebra.

   def sourceTracialRepresentation (θ : SourceCoordinate → ℝ) :
       TracialRepresentation (sourceAlgebra θ) where
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.TracialRepresentation, OAI.FiniteFactor.sourceAlgebra

2. theorem OAI.FiniteFactor.sourceTracialRepresentation_trace line 18
3. theorem OAI.FiniteFactor.sourceTracialRepresentation_normal line 22