OAI/Analysis/KadisonKastler/StateBicentralizerClosure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Closure of the bicentralizer in the faithful reference-vector norm

Near invariance of the reference state bounds the error caused by replacing an operator by a nearby bicentralizer element on that vector. No uniform operator-norm bound on the approximating elements is required.

  1. theorem OAI.KadisonKastler.stateBicentralizerMember_of_reference_approximation line 21