OAI/Analysis/KadisonKastler/StateVectorNormComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reference-vector norms under a state comparison

Norm convergence of vector states controls the squared vector norm of each fixed bounded operator. The conjugated version applies this to unitaries comparing two faithful states.

  1. theorem OAI.KadisonKastler.vector_norm_sq_le_state_distance line 21
  2. theorem OAI.KadisonKastler.conjugate_vector_norm_sq_le_state_distance line 38