OAI/Topology/CoarseAssembly/FiniteLocalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite partition localization of Fredholm cycles

This is the operator step used on each compact Rips component. A represented square partition of unity localizes the operator without changing its cycle class. The geometric partition and its propagation control are constructed separately.

  1. theorem OAI.CoarseAssembly.Analytic.localizedOperator_sub_eq line 21
  2. theorem OAI.CoarseAssembly.Analytic.localizedOperator_sub_compact line 38
  3. theorem OAI.CoarseAssembly.Analytic.localizedOperator_selfAdjoint line 45
  4. theorem OAI.CoarseAssembly.Analytic.localizedCycle_operator line 50
  5. theorem OAI.CoarseAssembly.Analytic.localizedCycle_class line 57