OAI/Topology/CoarseAssembly/PartitionCompression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The contraction estimate for finite partition localization

  1. theorem OAI.CoarseAssembly.DiscreteRoe.constantBlock_apply line 17
  2. theorem OAI.CoarseAssembly.DiscreteRoe.constantBlock_norm_le line 21
  3. theorem OAI.CoarseAssembly.DiscreteRoe.partitionMap_adjoint_apply line 24
  4. theorem OAI.CoarseAssembly.DiscreteRoe.partitionCompression_eq_sum line 29
  5. theorem OAI.CoarseAssembly.DiscreteRoe.partitionCompression_norm_le line 39