OAI/Topology/CoarseAssembly/DiagonalSpatialFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform diagonal families on the actual separated vertex union

  1. theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_apply line 18
  2. theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_norm_le line 23
  3. theorem OAI.CoarseAssembly.DiscreteRoe.rowVector_diagonalFamily line 28
  4. theorem OAI.CoarseAssembly.DiscreteRoe.entry_diagonalFamily_same line 35
  5. theorem OAI.CoarseAssembly.DiscreteRoe.entry_diagonalFamily_ne line 42
  6. theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_selfAdjoint line 51
  7. theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_propagation line 71