OAI/Topology/CoarseAssembly/PseudolocalAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Pseudolocal operators and the controlled structure algebra

  1. def OAI.CoarseAssembly.DiscreteRoe.Pseudolocal line 22
  2. theorem OAI.CoarseAssembly.DiscreteRoe.LocallyCompact.pseudolocal line 27
  3. theorem OAI.CoarseAssembly.DiscreteRoe.Pseudolocal.add line 31
  4. theorem OAI.CoarseAssembly.DiscreteRoe.Pseudolocal.mul line 43
  5. theorem OAI.CoarseAssembly.DiscreteRoe.Pseudolocal.smul line 55
  6. theorem OAI.CoarseAssembly.DiscreteRoe.pseudolocal_closed line 68
  7. def OAI.CoarseAssembly.DiscreteRoe.pseudolocalAlgebra line 75
  8. theorem OAI.CoarseAssembly.DiscreteRoe.pseudolocalAlgebra_closed line 102
  9. def OAI.CoarseAssembly.DiscreteRoe.StructureGenerator line 108
  10. def OAI.CoarseAssembly.DiscreteRoe.structureAlgebra line 112

    Source documentation

    The controlled pseudolocal algebra used to form the analytic-index quotient.

    def structureAlgebra : NonUnitalStarSubalgebra ℂ (Operator X H) :=
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator

  11. theorem OAI.CoarseAssembly.DiscreteRoe.structureAlgebra_pseudolocal line 115
  12. theorem OAI.CoarseAssembly.DiscreteRoe.roe_le_structureAlgebra line 124