OAI/Analysis/KadisonKastler/ProductBoundaryRoot.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Root selection with a passive boundary coordinate

  1. def OAI.KadisonKastler.firstBoundaryRootL line 21
  2. theorem OAI.KadisonKastler.firstBoundaryRootL_ae line 28
  3. theorem OAI.KadisonKastler.firstBoundaryRootL_norm_le line 39
  4. theorem OAI.KadisonKastler.firstBoundaryRootL_const line 51
  5. theorem OAI.KadisonKastler.firstBoundaryRootL_positive line 57
  6. theorem OAI.KadisonKastler.firstBoundaryRootL_module line 67
  7. theorem OAI.KadisonKastler.firstBoundaryRootL_translate line 82
  8. theorem OAI.KadisonKastler.firstBoundaryRootL_natural line 101
  9. def OAI.KadisonKastler.firstBoundaryScalarMean line 122