OAI/Analysis/JiangSu/CStarAlgebras/StateCoefficientApproximation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NuclearNorm.stateGNS_cyclic line 16
  2. structure OAI.NuclearNorm.StateRow line 26
  3. def OAI.NuclearNorm.StateRow.map line 31
  4. lemma OAI.NuclearNorm.StateRow.map_apply line 36
  5. def OAI.NuclearNorm.StateRow.scale line 51
  6. lemma OAI.NuclearNorm.StateRow.scale_map line 54
  7. def OAI.NuclearNorm.stateRowSum line 65
  8. lemma OAI.NuclearNorm.stateRowSum_scale line 68
  9. def OAI.NuclearNorm.stateRowCone line 76
  10. lemma OAI.NuclearNorm.stateRowCone_zero line 86
  11. lemma OAI.NuclearNorm.stateRowCone_row line 89
  12. lemma OAI.NuclearNorm.continuous_coefficient_tuple line 93
  13. theorem OAI.NuclearNorm.nuclear_state_coefficient_approximation line 104
  14. theorem OAI.NuclearNorm.simple_nuclear_state_coefficient_approximation line 147