OAI/Topology/CoarseAssembly/RoeCompactRows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compact rows and columns of locally compact finite-propagation operators

  1. theorem OAI.CoarseAssembly.DiscreteRoe.finite_column_operator line 14
  2. theorem OAI.CoarseAssembly.DiscreteRoe.finite_row_operator line 26
  3. theorem OAI.CoarseAssembly.DiscreteRoe.compact_column_of_propagation line 36
  4. theorem OAI.CoarseAssembly.DiscreteRoe.compact_row_of_propagation line 45
  5. theorem OAI.CoarseAssembly.DiscreteRoe.finiteDiagonal_mul_compact line 59
  6. theorem OAI.CoarseAssembly.DiscreteRoe.mul_finiteDiagonal_compact line 69