OAI/Analysis/ModularTheory/FiniteTrace.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Actual finite corners and their tracial vector functionals.

  1. def OAI.WeakPureInfiniteness.modularFiniteProjectionInCore line 19
  2. lemma OAI.WeakPureInfiniteness.modularFiniteProjectionInCore_star line 23
  3. lemma OAI.WeakPureInfiniteness.modularFiniteProjectionInCore_mul line 28
  4. abbrev OAI.WeakPureInfiniteness.ModularFiniteCorner line 34
  5. def OAI.WeakPureInfiniteness.modularFiniteCornerRepresentation line 38
  6. lemma OAI.WeakPureInfiniteness.modularFiniteCornerRepresentation_mem line 44
  7. lemma OAI.WeakPureInfiniteness.modularFiniteCornerRepresentation_right line 49
  8. lemma OAI.WeakPureInfiniteness.modularFiniteCornerRepresentation_left line 54
  9. def OAI.WeakPureInfiniteness.modularFiniteCornerFunctional line 59
  10. lemma OAI.WeakPureInfiniteness.representation_square_inner line 70
  11. lemma OAI.WeakPureInfiniteness.modularFiniteCornerFunctional_square line 80
  12. theorem OAI.WeakPureInfiniteness.modularFiniteCornerFunctional_tracial line 87
  13. lemma OAI.WeakPureInfiniteness.modularFiniteCornerFunctional_one line 107
  14. lemma OAI.WeakPureInfiniteness.modularWeightCutoffVector_succ_ne_zero line 115
  15. lemma OAI.WeakPureInfiniteness.modularCoreWeightVector_succ_ne_zero line 132