OAI/Topology/CoarseAssembly/CycleCompactPerturbation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact changes of a Fredholm operator

The straight-line path between operators differing by a compact operator preserves all three Fredholm defects. This is the normalization step used when discharging the odd coefficient and circle-index inputs.

  1. theorem OAI.CoarseAssembly.Analytic.compact_mul_right line 20
  2. theorem OAI.CoarseAssembly.Analytic.compact_mul_left line 23
  3. theorem OAI.CoarseAssembly.Analytic.compact_star_real_smul line 28
  4. def OAI.CoarseAssembly.Analytic.OddCycle.compactPerturbHomotopy line 33
  5. theorem OAI.CoarseAssembly.Analytic.OddCycle.compactPerturbHomotopy_start line 47
  6. theorem OAI.CoarseAssembly.Analytic.OddCycle.compactPerturbHomotopy_finish line 53
  7. theorem OAI.CoarseAssembly.Analytic.compactPerturb_class line 58