OAI/Analysis/BoundedHochschild/PositiveBlockRegularization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Remove strict positivity of the scalar block entries by norm limits.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.starAlgHom_real_one line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.positive_real_one line 24
  3. lemma OAI.BoundedHochschild.KadisonRingrose.positiveBlock_add_real_one line 30
  4. theorem OAI.BoundedHochschild.KadisonRingrose.positiveBlock_transfer line 35