OAI/Analysis/KadisonKastler/CountableUnitaryAssembly.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Assembling the dimension strata by a Hilbert direct sum

  1. def OAI.KadisonKastler.l2FiberUnitaryApply line 16
  2. theorem OAI.KadisonKastler.l2FiberUnitaryApply_apply line 20
  3. theorem OAI.KadisonKastler.norm_l2FiberUnitaryApply line 24
  4. def OAI.KadisonKastler.l2FiberUnitaryEquiv line 30
  5. def OAI.KadisonKastler.l2FiberUnitary line 52
  6. theorem OAI.KadisonKastler.l2FiberUnitary_apply line 55
  7. theorem OAI.KadisonKastler.norm_l2FiberUnitary_sub_one_le line 59