OAI/Analysis/KadisonKastler/WOTCoefficientDuality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient form of a weak-operator continuous functional

The defining weak topology first gives a finite coefficient expression. Finite polar duality then chooses coefficients with sharp Hilbert norms.

  1. theorem OAI.KadisonKastler.wot_functional_finite_coefficients line 22
  2. theorem OAI.KadisonKastler.wot_functional_sharp_coefficients line 62