OAI/Topology/CoarseAssembly/Averaging.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-quotient averaging operators

Normalized left translations and their lazy average act on the spatial fiber Hilbert spaces. They are contractions fixing the constant subspace. The strict norm bound off constants is kept as the precise published Kazhdan-gap input, rather than assuming any Roe transfer conclusion.

  1. def OAI.CoarseAssembly.constantProjection line 25
  2. theorem OAI.CoarseAssembly.constantProjection_idempotent line 29
  3. theorem OAI.CoarseAssembly.constantProjection_norm_le line 34
  4. def OAI.CoarseAssembly.leftTranslation line 42
  5. theorem OAI.CoarseAssembly.leftTranslation_constant line 46
  6. theorem OAI.CoarseAssembly.leftTranslation_projection line 50
  7. theorem OAI.CoarseAssembly.projection_leftTranslation line 59
  8. def OAI.CoarseAssembly.meanTranslation line 83
  9. def OAI.CoarseAssembly.lazyAverage line 87
  10. theorem OAI.CoarseAssembly.meanTranslation_norm_le line 91
  11. theorem OAI.CoarseAssembly.lazyAverage_norm_le line 112
  12. theorem OAI.CoarseAssembly.lazyAverage_projection line 122
  13. theorem OAI.CoarseAssembly.projection_lazyAverage line 135