OAI/Analysis/Unitarizability/HilbertSum.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded Hilbert direct sums. The component implementers are never summed and need not be uniformly bounded.

  1. abbrev OAI.Dixmier.HilbertSum.Space line 15
  2. def OAI.Dixmier.HilbertSum.inclusion line 17
  3. def OAI.Dixmier.HilbertSum.evaluation line 19
  4. theorem OAI.Dixmier.HilbertSum.inclusion_apply line 21
  5. theorem OAI.Dixmier.HilbertSum.evaluation_apply line 22
  6. def OAI.Dixmier.HilbertSum.boundedSum line 24
  7. theorem OAI.Dixmier.HilbertSum.boundedSum_apply line 27
  8. theorem OAI.Dixmier.HilbertSum.boundedSum_norm_le line 31
  9. theorem OAI.Dixmier.HilbertSum.unitary_bound line 35
  10. def OAI.Dixmier.HilbertSum.representation line 42
  11. theorem OAI.Dixmier.HilbertSum.representation_apply line 51
  12. theorem OAI.Dixmier.HilbertSum.representation_norm_map line 55
  13. def OAI.Dixmier.HilbertSum.cocycle line 64
  14. theorem OAI.Dixmier.HilbertSum.cocycle_apply line 69
  15. theorem OAI.Dixmier.HilbertSum.cocycle_one line 73
  16. theorem OAI.Dixmier.HilbertSum.cocycle_identity line 77
  17. theorem OAI.Dixmier.HilbertSum.representation_inclusion line 88
  18. def OAI.Dixmier.HilbertSum.compression line 96
  19. theorem OAI.Dixmier.HilbertSum.compression_norm_le line 99
  20. theorem OAI.Dixmier.HilbertSum.compression_conjugate line 108
  21. theorem OAI.Dixmier.HilbertSum.compression_implementer line 117
  22. theorem OAI.Dixmier.HilbertSum.separableSpace line 134

    Source documentation

    Countably many separable fibres have a separable Hilbert sum. The proof uses the dense span of coordinate inclusions and convergence of finite sums.

    theorem separableSpace [Countable I] [∀ i, TopologicalSpace.SeparableSpace (E i)] :
    TopologicalSpace.SeparableSpace (Space E) := by
…

    Mentions: OAI.Dixmier.HilbertSum.Space