OAI/Analysis/Commutator/L2InfiniteSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.Decomposable.singleL line 25
  2. def OAI.Kadison.Decomposable.evalL line 28
  3. lemma OAI.Kadison.Decomposable.inner_singleL line 32
  4. lemma OAI.Kadison.Decomposable.evalL_singleL line 46
  5. def OAI.Kadison.Decomposable.singleLI line 66
  6. lemma OAI.Kadison.Decomposable.singleLI_orthogonal line 72
  7. lemma OAI.Kadison.Decomposable.evalL_separates line 78
  8. lemma OAI.Kadison.Decomposable.singleLI_total line 93
  9. def OAI.Kadison.Decomposable.infiniteSumEquiv line 113