OAI/Analysis/CharacterCriterion/EndpointMultiplicity.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.DropMatrixRepresentations.left_injective line 40
  2. lemma OAI.KirchbergRordam.DropMatrixRepresentations.right_injective line 46
  3. def OAI.KirchbergRordam.DropMatrixRepresentations.leftValue line 53
  4. lemma OAI.KirchbergRordam.DropMatrixRepresentations.leftValue_spec line 55
  5. def OAI.KirchbergRordam.DropMatrixRepresentations.rightValue line 62
  6. lemma OAI.KirchbergRordam.DropMatrixRepresentations.rightValue_spec line 64
  7. def OAI.KirchbergRordam.DropMatrixRepresentations.leftEvaluation line 71
  8. def OAI.KirchbergRordam.DropMatrixRepresentations.rightEvaluation line 79
  9. lemma OAI.KirchbergRordam.DropMatrixRepresentations.two_three line 87
  10. def OAI.KirchbergRordam.DropMatrixRepresentations.blockRepresentation line 92
  11. def OAI.KirchbergRordam.DropMatrixRepresentations.representation line 96
  12. def OAI.KirchbergRordam.EndpointMultiplicity.leftExpand line 110
  13. def OAI.KirchbergRordam.EndpointMultiplicity.rightExpand line 122
  14. lemma OAI.KirchbergRordam.EndpointMultiplicity.leftExpand_matrix line 134
  15. lemma OAI.KirchbergRordam.EndpointMultiplicity.rightExpand_matrix line 146
  16. def OAI.KirchbergRordam.EndpointMultiplicity.constHom line 159
  17. def OAI.KirchbergRordam.EndpointMultiplicity.prodUnitary line 167
  18. lemma OAI.KirchbergRordam.EndpointMultiplicity.map_conj line 169
  19. def OAI.KirchbergRordam.EndpointMultiplicity.duplicate line 173
  20. def OAI.KirchbergRordam.EndpointMultiplicity.duplicateUnitary line 176
  21. lemma OAI.KirchbergRordam.EndpointMultiplicity.conj_duplicate line 179
  22. def OAI.KirchbergRordam.EndpointMultiplicity.leftBase line 197
  23. def OAI.KirchbergRordam.EndpointMultiplicity.rightBase line 201
  24. lemma OAI.KirchbergRordam.EndpointMultiplicity.leftBase_commute line 205
  25. lemma OAI.KirchbergRordam.EndpointMultiplicity.rightBase_commute line 221
  26. def OAI.KirchbergRordam.EndpointMultiplicity.leftRep line 238
  27. def OAI.KirchbergRordam.EndpointMultiplicity.rightRep line 241
  28. lemma OAI.KirchbergRordam.EndpointMultiplicity.leftRep_commute line 244
  29. lemma OAI.KirchbergRordam.EndpointMultiplicity.rightRep_commute line 255
  30. lemma OAI.KirchbergRordam.EndpointMultiplicity.commutator_approx line 268
  31. lemma OAI.KirchbergRordam.EndpointMultiplicity.duplicate_difference line 282
  32. lemma OAI.KirchbergRordam.EndpointMultiplicity.leftRep_bound line 288
  33. lemma OAI.KirchbergRordam.EndpointMultiplicity.rightRep_bound line 295