OAI/Analysis/KadisonKastler/ScalarL2Multiplication.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Bounded scalar multiplication on L2

This supplies weak continuity of multiplication by a fixed boundary function when passing the averaging module identity to the limit.

  1. def OAI.KadisonKastler.scalarL2Mul line 20
  2. theorem OAI.KadisonKastler.scalarL2Mul_ae line 23
  3. theorem OAI.KadisonKastler.norm_scalarL2Mul_le line 26
  4. theorem OAI.KadisonKastler.scalarL2Mul_add line 33
  5. theorem OAI.KadisonKastler.scalarL2Mul_smul line 42
  6. def OAI.KadisonKastler.scalarL2MulL line 50
  7. theorem OAI.KadisonKastler.scalarL2MulL_apply line 58
  8. theorem OAI.KadisonKastler.scalarInfinityToL2_mul line 63
  9. theorem OAI.KadisonKastler.scalarInfinityMul_of_weak_limits line 70