OAI/Topology/CoarseAssembly/ToeplitzCompression.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fredholmness of scalar-unitary Toeplitz compressions

  1. def OAI.CoarseAssembly.Analytic.toeplitzCompression line 13
  2. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_star line 15
  3. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_mul line 19
  4. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_left_defect line 26
  5. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_compact_defects line 36
  6. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_fredholm line 57
  7. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_unitary line 64