OAI/Topology/CoarseAssembly/PartitionCompactPerturbation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact perturbations through the actual localization operators

  1. theorem OAI.CoarseAssembly.isometricExtension_sub line 16
  2. theorem OAI.CoarseAssembly.isometricExtension_sub_compact line 27
  3. theorem OAI.CoarseAssembly.DiscreteRoe.partitionCompression_sub line 37
  4. theorem OAI.CoarseAssembly.DiscreteRoe.partitionCompression_sub_compact line 45
  5. theorem OAI.CoarseAssembly.DiscreteRoe.localizedSpatialOperator_sub_compact line 52
  6. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_compactPerturb line 66
  7. theorem OAI.CoarseAssembly.Rips.ampleRipsOperator_compactPerturb line 79