OAI/Analysis/KadisonKastler/StateBicentralizerAdjoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Adjoint stability of state-sequence bicentralizers

Approximate preservation of the faithful state supplies the extra norm control needed to pass from strong convergence to adjoint convergence.

  1. theorem OAI.KadisonKastler.adjoint_vector_difference_sq_le line 21
  2. theorem OAI.KadisonKastler.stateConjugate_adjoint_difference_sq_le line 40