OAI/Analysis/KadisonKastler/HermitianSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Separating a self-adjoint element from a closed star subalgebra

Hahn–Banach on the Banach-space quotient gives a norm-one functional annihilating the source. Its Hermitian part still separates a self-adjoint element. The compact annihilator ball then supplies an extreme separator.

  1. def OAI.KadisonKastler.conjugateFunctional line 20
  2. theorem OAI.KadisonKastler.conjugateFunctional_norm_le line 26
  3. theorem OAI.KadisonKastler.exists_hermitian_separator line 33
  4. theorem OAI.KadisonKastler.exists_extreme_hermitian_separator line 95