OAI/Analysis/KadisonKastler/TwoCornerStrictContraction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Strict decrease after removing a bounded-below off-diagonal corner

The spatial innerness argument uses a self-adjoint two-by-two operator whose off-diagonal corner is bounded below on both summands. Removing that corner strictly decreases the norm. The estimate is purely a C-star algebra calculation.

  1. theorem OAI.KadisonKastler.projection_column_square line 21
  2. theorem OAI.KadisonKastler.norm_projection_diagonal_sq_le line 31
  3. theorem OAI.KadisonKastler.norm_two_corner_diagonal_lt line 58