OAI/Topology/CoarseAssembly/EssentialToeplitz.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Toeplitz Fredholmness before choosing an involution

A self-adjoint operator with compact square defect suffices. This lets the index be defined using the explicit, continuous cut-down operator.

  1. theorem OAI.CoarseAssembly.Analytic.positiveProjection_sub line 18
  2. theorem OAI.CoarseAssembly.Analytic.compact_toeplitz_sub line 23
  3. theorem OAI.CoarseAssembly.Analytic.compact_star_toeplitz_sub line 33
  4. theorem OAI.CoarseAssembly.Analytic.essentialToeplitz_compact_defects line 39