OAI/Analysis/KadisonKastler/RowEnergyBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Complete norm control of the finite row energies.

  1. theorem OAI.KadisonKastler.algebraRow_norm_le_one line 25
  2. theorem OAI.KadisonKastler.rowAdjointVector_map_bound line 42
  3. theorem OAI.KadisonKastler.CompletelyBoundedBy.rowEnergy line 65