OAI/Analysis/KadisonKastler/ProjectionNormGap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Localizing the Hilbert-space norm-gap argument to a projection range.

  1. theorem OAI.KadisonKastler.projection_fixed_on_range line 14
  2. theorem OAI.KadisonKastler.norm_comp_projection_eq_norm_restrict line 21
  3. theorem OAI.KadisonKastler.projection_norm_equality_no_spectral_gap line 40