OAI/Analysis/BoundedHochschild/OperatorSystemFunctionals.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positive scalar functionals on unital self-adjoint linear subspaces. The extension uses real Hahn–Banach on the self-adjoint part.

  1. def OAI.BoundedHochschild.KadisonRingrose.operatorSystemRealPart line 16
  2. def OAI.BoundedHochschild.KadisonRingrose.operatorSystemRealInclusion line 19
  3. lemma OAI.BoundedHochschild.KadisonRingrose.positive_subspace_selfAdjoint_im line 25
  4. lemma OAI.BoundedHochschild.KadisonRingrose.positive_subspace_real_bound line 42
  5. def OAI.BoundedHochschild.KadisonRingrose.operatorSystemRealFunctional line 70
  6. lemma OAI.BoundedHochschild.KadisonRingrose.selfAdjoint_nonneg_of_norm_le line 78