OAI/Analysis/OperatorAlgebra/FiniteOperatorPredual.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite sums of vector functionals, with their norm as functionals on bounded operators, have bounded operators as their continuous dual. This finite predual is sufficient for the convex separation step in the hypertrace argument; no trace-class completion is required here.

  1. lemma OAI.WeakPureInfiniteness.operatorCoefficient_norm_le line 21
  2. abbrev OAI.WeakPureInfiniteness.finiteOperatorPredual line 30
  3. instance OAI.WeakPureInfiniteness.finitePredualNormed line 33
  4. instance OAI.WeakPureInfiniteness.finitePredualComplex line 36
  5. instance OAI.WeakPureInfiniteness.finitePredualReal line 39
  6. def OAI.WeakPureInfiniteness.finiteOperatorCoefficient line 42
  7. lemma OAI.WeakPureInfiniteness.finiteOperatorCoefficient_add_left line 46
  8. lemma OAI.WeakPureInfiniteness.finiteOperatorCoefficient_add_right line 53
  9. lemma OAI.WeakPureInfiniteness.finiteOperatorCoefficient_smul_left line 61
  10. lemma OAI.WeakPureInfiniteness.finiteOperatorCoefficient_smul_right line 69
  11. def OAI.WeakPureInfiniteness.predualFunctionalRight line 76
  12. def OAI.WeakPureInfiniteness.predualFunctionalForm line 88
  13. def OAI.WeakPureInfiniteness.finitePredualOperator line 102
  14. lemma OAI.WeakPureInfiniteness.finitePredualOperator_coefficient line 105
  15. theorem OAI.WeakPureInfiniteness.finitePredualOperator_represents line 112
  16. theorem OAI.WeakPureInfiniteness.finitePredual_real_duality line 127