OAI/Topology/CoarseAssembly/SpatialBlocks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Controlled block matrices on the spatial vertex module

The bounded block-matrix construction is transported through the explicit Hilbert-sum equivalence. Its vertex entries are the entries of the original blocks, which allows propagation and local compactness to be checked there.

  1. theorem OAI.CoarseAssembly.flattenOperator_apply line 21
  2. theorem OAI.CoarseAssembly.flattenOperator_norm_le line 27
  3. theorem OAI.CoarseAssembly.rowVector_single_same line 40
  4. theorem OAI.CoarseAssembly.rowVector_single_ne line 55
  5. def OAI.CoarseAssembly.spatialBlocks line 71
  6. theorem OAI.CoarseAssembly.spatialBlocks_norm_le line 75
  7. theorem OAI.CoarseAssembly.spatialBlocks_apply line 80
  8. theorem OAI.CoarseAssembly.spatialBlocks_single line 84