OAI/Analysis/FactorGeneration/CoordinateUnitaries.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Complete each supported partial unitary by the identity on its orthogonal complement. If the quotient support is one, the quotient value is unchanged.

  1. def OAI.Generator.Tracial.PartialUnitary.completed line 16
  2. theorem OAI.Generator.Tracial.PartialUnitary.completed_unitary line 19
  3. theorem OAI.Generator.Tracial.PartialUnitary.completed_mem line 34
  4. def OAI.Generator.Tracial.boundedCompletedUnitary line 42
  5. theorem OAI.Generator.Tracial.boundedCompletedUnitary_apply line 45
  6. theorem OAI.Generator.Tracial.boundedCompletedUnitary_unitary line 48
  7. theorem OAI.Generator.Tracial.quotient_completed_eq line 52
  8. theorem OAI.Generator.Tracial.bounded_unitary_of_coordinates line 68
  9. theorem OAI.Generator.Tracial.quotient_unitary_of_coordinates line 74
  10. theorem OAI.Generator.Tracial.bounded_coordinate_unitaries_inclusion line 82
  11. theorem OAI.Generator.Tracial.exists_coordinate_ordered_unitary line 116
  12. theorem OAI.Generator.Tracial.exists_coordinate_reduced_unitary line 149
  13. theorem OAI.Generator.Tracial.coordinate_haar_endpoints_of_coordinates line 187
  14. theorem OAI.Generator.Tracial.coordinate_haar_endpoints_of_dense_family line 216
  15. theorem OAI.Generator.Tracial.exists_coordinate_haar_endpoints line 232