OAI/Analysis/KadisonSimilarity/Representation/ConcretePredualRestriction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Normality of a trace restricts to a concrete von Neumann subalgebra. Restriction sends each vector functional to the same vector functional, and therefore preserves their closed span.

  1. def OAI.KadisonSimilarity.concreteInclusionCLM line 19
  2. def OAI.KadisonSimilarity.normalRestriction line 26
  3. theorem OAI.KadisonSimilarity.normalRestriction_apply line 31
  4. theorem OAI.KadisonSimilarity.normalRestriction_coefficient line 35
  5. theorem OAI.KadisonSimilarity.normalRestriction_mem line 38
  6. def OAI.KadisonSimilarity.predualRestriction line 51
  7. theorem OAI.KadisonSimilarity.predualRestriction_apply line 55
  8. def OAI.KadisonSimilarity.includedPositiveTrace line 59
  9. theorem OAI.KadisonSimilarity.includedPositiveTrace_apply line 64
  10. theorem OAI.KadisonSimilarity.includedPositiveTrace_normal line 68
  11. theorem OAI.KadisonSimilarity.includedPositiveTrace_hasNormalGNS line 76