OAI/Topology/CoarseAssembly/CompactFunctionalCalculus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Functional calculus preserves compact self-adjoint operators

Compact operators whose adjoints are compact form a closed star algebra. The nonunital functional calculus stays in that algebra. This supplies the compactness step in the remaining normalization of the odd coefficient.

  1. def OAI.CoarseAssembly.Analytic.compactOperatorAlgebra line 20
  2. theorem OAI.CoarseAssembly.Analytic.compactOperatorAlgebra_closed line 38
  3. theorem OAI.CoarseAssembly.Analytic.compact_cfcₙ line 44
  4. theorem OAI.CoarseAssembly.Analytic.compact_cfc line 51