OAI/Analysis/TracialSplitting/CoefficientBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NuclearTrace.coefficientMap line 76
  2. lemma OAI.NuclearTrace.coefficientMap_star line 83
  3. lemma OAI.NuclearTrace.coefficientMap_selfAdjoint line 96
  4. def OAI.NuclearTrace.algebraTensorVector line 110
  5. lemma OAI.NuclearTrace.algebraTensorVector_tmul line 114
  6. lemma OAI.NuclearTrace.algebraTensorVector_dense line 118
  7. lemma OAI.NuclearTrace.gns_commutant_coefficient line 151
  8. lemma OAI.NuclearTrace.spatial_coefficient_value line 169
  9. theorem OAI.NuclearTrace.nuclear_coefficient_dual_bound line 208
  10. lemma OAI.NuclearTrace.linear_bound_of_seminorm_ball line 296
  11. theorem OAI.NuclearTrace.seminorm_cone_approximation_of_dual line 330
  12. lemma OAI.CurrentMain.traceOneNorm_smul_real line 388
  13. lemma OAI.CurrentMain.traceOneNorm_le_norm line 392
  14. def OAI.CurrentMain.tracialOneSeminorm line 396
  15. lemma OAI.CurrentMain.tracialOneSeminorm_apply line 403
  16. lemma OAI.CurrentMain.tracialOneSeminorm_continuous line 406
  17. lemma OAI.CurrentMain.tracialOneSeminorm_of_nonneg line 413