OAI/Topology/CoarseAssembly/RoeInclusion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The reduced Roe map for an actual injective nonexpanding inclusion

Extension by zero preserves each matrix entry on the image, and all other entries vanish. Thus propagation and local compactness are proved directly before extending to the norm closure.

  1. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_adjoint_apply line 27
  2. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_entry line 38
  3. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_entry_row_zero line 46
  4. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_entry_col_zero line 52
  5. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_compactEntries line 65
  6. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_propagation line 81
  7. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_generator line 94
  8. theorem OAI.CoarseAssembly.DiscreteRoe.inclusion_mapsToRoe line 102