OAI/Topology/CoarseAssembly/KernelProjection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The finite-rank kernel correction

For a self-adjoint operator with compact square defect, the orthogonal projection onto its kernel is compact. Adding that projection removes the kernel and preserves self-adjointness and the compact square defect.

  1. def OAI.CoarseAssembly.Analytic.kernelClosedSubmodule line 19
  2. def OAI.CoarseAssembly.Analytic.kernelProjection line 22
  3. theorem OAI.CoarseAssembly.Analytic.kernelProjection_selfAdjoint line 24
  4. theorem OAI.CoarseAssembly.Analytic.mul_kernelProjection line 27
  5. theorem OAI.CoarseAssembly.Analytic.kernelProjection_mul line 31
  6. theorem OAI.CoarseAssembly.Analytic.kernelProjection_sq line 36
  7. theorem OAI.CoarseAssembly.Analytic.kernelProjection_compact line 40
  8. theorem OAI.CoarseAssembly.Analytic.kernel_corrected_eq_zero line 50
  9. theorem OAI.CoarseAssembly.Analytic.kernel_corrected_injective line 67
  10. theorem OAI.CoarseAssembly.Analytic.kernel_corrected_selfAdjoint line 74
  11. theorem OAI.CoarseAssembly.Analytic.kernel_corrected_compact_square line 78