OAI/Topology/CoarseAssembly/SeparatedFamilyBoundary.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A Roe boundary class from a uniformly controlled separated family

The compact component defects need not decay in norm. Their direct sum is nevertheless a finite-propagation operator with compact matrix entries, which is the local compactness needed for the whole-union Roe algebra.

  1. theorem OAI.CoarseAssembly.DiscreteRoe.separatedMetric_closedBall_finite line 25
  2. theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_square_mem_roe line 36
  3. theorem OAI.CoarseAssembly.DiscreteRoe.separatedFamilyMultiplier_selfAdjoint line 61