OAI/Analysis/BoundedHochschild/PositiveDecomposition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Decomposition of continuous functionals into positive functionals.

  1. lemma OAI.HochschildPositiveDecomposition.norm_pair_shift line 33
  2. def OAI.HochschildPositiveDecomposition.shiftEmbedding line 61
  3. lemma OAI.HochschildPositiveDecomposition.shiftEmbedding_injective line 66
  4. lemma OAI.HochschildPositiveDecomposition.exists_pair_extension line 79
  5. lemma OAI.HochschildPositiveDecomposition.norm_orderUnit_sub line 112
  6. lemma OAI.HochschildPositiveDecomposition.pair_nonneg line 124
  7. lemma OAI.HochschildPositiveDecomposition.exists_real_positive_difference line 141
  8. def OAI.HochschildPositiveDecomposition.complexify line 169
  9. lemma OAI.HochschildPositiveDecomposition.complexify_apply line 175
  10. lemma OAI.HochschildPositiveDecomposition.complexify_selfAdjoint line 178
  11. def OAI.HochschildPositiveDecomposition.complexifyPositive line 187
  12. lemma OAI.HochschildPositiveDecomposition.complexifyPositive_apply line 200
  13. def OAI.HochschildPositiveDecomposition.realRestriction line 207
  14. def OAI.HochschildPositiveDecomposition.imagRestriction line 210
  15. lemma OAI.HochschildPositiveDecomposition.realRestriction_apply line 213
  16. lemma OAI.HochschildPositiveDecomposition.imagRestriction_apply line 215
  17. lemma OAI.HochschildPositiveDecomposition.realRestriction_norm line 218
  18. lemma OAI.HochschildPositiveDecomposition.imagRestriction_norm line 222
  19. lemma OAI.HochschildPositiveDecomposition.real_imag_restriction_decomposition line 227
  20. theorem OAI.HochschildPositiveDecomposition.exists_four_positive line 243