OAI/Topology/CoarseAssembly/LocalizationNormContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Localization is contractive in the Fredholm operator

  1. theorem OAI.CoarseAssembly.DiscreteRoe.localizedSpatialOperator_sub_norm_le line 15
  2. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientExtension_sub_norm_le line 24
  3. theorem OAI.CoarseAssembly.Rips.ampleRipsOperator_homotopy_norm_le line 38