OAI/Analysis/KadisonSimilarity/Tracial/TracialGeometrySupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The normal tracial geometry supplies the propagation support input. Positivity of its trace follows directly from the Hilbert inner product.

  1. def OAI.KadisonSimilarity.TracialCornerGeometry.positiveTrace line 20
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.positiveTrace_apply line 26
  3. theorem OAI.KadisonSimilarity.TracialCornerGeometry.rightSupportInput_of_normal_range line 30