OAI/Analysis/KadisonKastler/FreeModelCutBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Norm estimates for actual cuts in the free diagonal model

  1. theorem OAI.KadisonKastler.FreeDiagonalModel.norm_noPreservationSum_le line 23
  2. theorem OAI.KadisonKastler.FreeDiagonalModel.norm_preservationSum_le line 46