OAI/Analysis/CharacterCriterion/MatrixPaths.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.UnitaryPaths.phase_continuous line 36
  2. lemma OAI.KirchbergRordam.UnitaryPaths.phase_zero line 37
  3. lemma OAI.KirchbergRordam.UnitaryPaths.phase_one line 38
  4. lemma OAI.KirchbergRordam.UnitaryPaths.phase_unitary line 39
  5. lemma OAI.KirchbergRordam.UnitaryPaths.involutionValue_continuous line 46
  6. lemma OAI.KirchbergRordam.UnitaryPaths.involutionValue_unitary line 50
  7. lemma OAI.KirchbergRordam.MatrixPermutationPath.perm_one line 95
  8. lemma OAI.KirchbergRordam.MatrixPermutationPath.perm_mul line 99
  9. lemma OAI.KirchbergRordam.MatrixPermutationPath.perm_swap_selfadjoint line 104
  10. theorem OAI.KirchbergRordam.MatrixPermutationPath.joined_one_perm line 110
  11. lemma OAI.KirchbergRordam.MatrixPermutationPath.perm_conjugation line 119
  12. lemma OAI.KirchbergRordam.MatrixDiagonalPath.block_apply line 137
  13. lemma OAI.KirchbergRordam.MatrixDiagonalPath.block_injective line 139
  14. lemma OAI.KirchbergRordam.MatrixDiagonalPath.evaluationBlock_continuous line 147
  15. lemma OAI.KirchbergRordam.MatrixDiagonalPath.diagonal_injective line 152
  16. lemma OAI.KirchbergRordam.MatrixDiagonalPath.interpolate_zero line 164
  17. lemma OAI.KirchbergRordam.MatrixDiagonalPath.interpolate_one line 178
  18. lemma OAI.KirchbergRordam.MatrixDiagonalPath.interpolate_continuous line 196
  19. lemma OAI.KirchbergRordam.MatrixBlockReindex.sumBlock_ll line 225
  20. lemma OAI.KirchbergRordam.MatrixBlockReindex.sumBlock_lr line 227
  21. lemma OAI.KirchbergRordam.MatrixBlockReindex.sumBlock_rl line 229
  22. lemma OAI.KirchbergRordam.MatrixBlockReindex.sumBlock_rr line 231
  23. lemma OAI.KirchbergRordam.MatrixBlockReindex.left_apply line 234
  24. lemma OAI.KirchbergRordam.MatrixBlockReindex.right_apply line 238
  25. def OAI.KirchbergRordam.MatrixBlockReindex.repackLeft line 244
  26. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackLeft_low line 254
  27. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackLeft_full line 277
  28. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackLeft_entry line 301
  29. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackLeft_matrix line 321
  30. def OAI.KirchbergRordam.MatrixBlockReindex.repackRight line 331
  31. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackRight_low line 343
  32. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackRight_full line 366
  33. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackRight_entry line 390
  34. lemma OAI.KirchbergRordam.MatrixBlockReindex.repackRight_matrix line 410