OAI/Analysis/TracialSplitting/TraceNormalization.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Pureness.TracialState.norm_apply_le_four line 47
  2. def OAI.Pureness.TracialState.toWeakDual line 63
  3. lemma OAI.Pureness.TracialState.toWeakDual_apply line 67
  4. lemma OAI.Pureness.TracialState.toWeakDual_injective line 70
  5. instance OAI.Pureness.(instance at line 78) line 78
  6. lemma OAI.Pureness.TracialState.isEmbedding_toWeakDual line 81
  7. def OAI.Pureness.tracialStateCarrier line 85
  8. def OAI.Pureness.tracialStateFromWeakDual line 88
  9. lemma OAI.Pureness.range_tracialState_toWeakDual line 101
  10. lemma OAI.Pureness.isClosed_tracialStateCarrier line 112
  11. lemma OAI.Pureness.isCompact_tracialStateCarrier line 133
  12. instance OAI.Pureness.(instance at line 143) line 143
  13. lemma OAI.Pureness.TracialState.continuous_eval line 148
  14. theorem OAI.Pureness.isCompact_tracialState_univ line 152
  15. lemma OAI.Pureness.convex_tracialStateCarrier line 161
  16. def OAI.NuclearTrace.traceTupleCost line 185
  17. lemma OAI.NuclearTrace.traceTupleCost_continuous line 195
  18. lemma OAI.NuclearTrace.traceTupleCost_eq line 201
  19. lemma OAI.NuclearTrace.traceTupleCost_continuous_right line 206
  20. lemma OAI.NuclearTrace.traceTupleCost_convex_right line 212
  21. theorem OAI.NuclearTrace.nuclear_uniform_tracial_coefficient_approximation line 226