OAI/Analysis/KadisonKastler/BicentralizerStateCauchy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Comparing faithful states gives Cauchy conjugates of bicentralizer elements

Norm convergence of the conjugated states yields the convergence used in canonical state transport.

  1. theorem OAI.KadisonKastler.conjugates_vector_difference_sq_le line 22
  2. theorem OAI.KadisonKastler.stateBicentralizerMember.conjugates_cauchy line 63