OAI/Topology/CoarseAssembly/ControlledMatrices.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded operators from controlled block matrices

A finite-propagation matrix has uniformly bounded row and column supports. Cauchy--Schwarz and finite double counting construct its bounded operator directly. This supplies the boundedness step of the transfer lift without an auxiliary edge colouring.

  1. theorem OAI.CoarseAssembly.norm_sum_sq_le_card line 20
  2. theorem OAI.CoarseAssembly.sum_neighbors_le line 33
  3. def OAI.CoarseAssembly.matrixRow line 61
  4. theorem OAI.CoarseAssembly.matrixRow_norm_sq line 65
  5. theorem OAI.CoarseAssembly.matrix_finite_norm_sq line 83
  6. def OAI.CoarseAssembly.controlledMatrixLinear line 103
  7. theorem OAI.CoarseAssembly.controlledMatrixLinear_norm_le line 124
  8. def OAI.CoarseAssembly.controlledMatrix line 137
  9. theorem OAI.CoarseAssembly.controlledMatrix_norm_le line 145
  10. theorem OAI.CoarseAssembly.controlledMatrix_apply line 154