OAI/Analysis/KadisonSimilarity/Representation/CenteredProjectionNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Centering an orthogonal projection at one half gives norm at most one half.

  1. theorem OAI.KadisonSimilarity.norm_projection_sub_half_le line 13