OAI/Topology/CoarseAssembly/FredholmParametrix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact parametrices and finite-dimensional defects

These are the finite-dimensional analytic ingredients for the scalar-unitary index pairing. No index-pairing conclusion is assumed here.

  1. theorem OAI.CoarseAssembly.Analytic.finiteDimensional_ker_of_compact_parametrix line 18
  2. theorem OAI.CoarseAssembly.Analytic.compact_idempotent_finiteRange line 32
  3. theorem OAI.CoarseAssembly.Analytic.fredholm_of_finite_parametrix line 45
  4. theorem OAI.CoarseAssembly.Analytic.isFredholm_of_compact_essential_unitary line 55