OAI/Analysis/KadisonKastler/HilbertNormGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar Hilbert-space norm estimates for the spectral-cut step in Paulsen's averaging proof (JFA157 (1998), proof of Theorem5.8, pp379–380).

  1. theorem OAI.KadisonKastler.opNorm_sq_le_of_pointwise_sq_le line 18
  2. theorem OAI.KadisonKastler.not_uniform_positive_norm_gap line 28
  3. theorem OAI.KadisonKastler.projection_complement_norm_sq line 41
  4. theorem OAI.KadisonKastler.norm_preserving_projection_no_coercive_complement line 53