OAI/Analysis/Commutator/PolarDecomposition.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.Polar.norm_abs_apply line 17
  2. def OAI.Kadison.Polar.initial line 29
  3. instance OAI.Kadison.Polar.(instance at line 32) line 32
  4. def OAI.Kadison.Polar.absToInitial line 35
  5. lemma OAI.Kadison.Polar.absToInitial_dense line 39
  6. def OAI.Kadison.Polar.initialMap line 51
  7. lemma OAI.Kadison.Polar.initialMap_abs line 54
  8. lemma OAI.Kadison.Polar.initialMap_norm line 61
  9. def OAI.Kadison.Polar.partialIsometry line 68
  10. lemma OAI.Kadison.Polar.partialIsometry_mem line 71
  11. lemma OAI.Kadison.Polar.factorization line 76
  12. lemma OAI.Kadison.Polar.initialMap_adjoint_comp line 81
  13. lemma OAI.Kadison.Polar.partialIsometry_initial line 85
  14. lemma OAI.Kadison.Polar.partialIsometry_mul_initial line 94
  15. lemma OAI.Kadison.Polar.partialIsometry_final_projection line 101
  16. lemma OAI.Kadison.Polar.initial_invariant line 110
  17. lemma OAI.Kadison.Polar.projection_commutes line 119
  18. lemma OAI.Kadison.Polar.partialIsometry_commutes line 130
  19. theorem OAI.Kadison.Polar.partialIsometry_mem_vonNeumann line 161