OAI/Topology/CoarseAssembly/BinaryHilbertSum.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Concrete binary sums of the Hilbert spaces of analytic cycles

  1. abbrev OAI.CoarseAssembly.Analytic.binaryHilbertSpace line 14
  2. def OAI.CoarseAssembly.Analytic.binaryLeft line 23
  3. def OAI.CoarseAssembly.Analytic.binaryRight line 29
  4. theorem OAI.CoarseAssembly.Analytic.binaryLeft_adjoint line 35
  5. theorem OAI.CoarseAssembly.Analytic.binaryRight_adjoint line 44
  6. theorem OAI.CoarseAssembly.Analytic.binaryLeft_right line 53
  7. theorem OAI.CoarseAssembly.Analytic.binary_exhaustive line 60
  8. def OAI.CoarseAssembly.Analytic.binaryBlock line 71

    Source documentation

    Block diagonal operators, on the actual Hilbert sum.

    def binaryBlock (T : End H) (S : End K) : End (binaryHilbertSpace H K) :=
…

    Mentions: OAI.CoarseAssembly.Analytic.End, OAI.CoarseAssembly.Analytic.binaryHilbertSpace

  9. theorem OAI.CoarseAssembly.Analytic.binaryBlock_apply line 74
  10. theorem OAI.CoarseAssembly.Analytic.binaryBlock_add line 82
  11. theorem OAI.CoarseAssembly.Analytic.binaryBlock_sub line 89
  12. theorem OAI.CoarseAssembly.Analytic.binaryBlock_mul line 96
  13. theorem OAI.CoarseAssembly.Analytic.binaryBlock_one line 104
  14. theorem OAI.CoarseAssembly.Analytic.binaryBlock_zero line 109
  15. theorem OAI.CoarseAssembly.Analytic.binaryBlock_star line 114
  16. theorem OAI.CoarseAssembly.Analytic.binaryBlock_smul line 118
  17. def OAI.CoarseAssembly.Analytic.binaryBlockHom line 124
  18. theorem OAI.CoarseAssembly.Analytic.binaryBlock_compact line 135