OAI/Topology/CoarseAssembly/TransferLift.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The controlled lift and its exact compression

The lift is constructed as a bounded block matrix. Its scalar coefficient condition proves local compactness, while preservation of constant-fiber vectors proves the compression identity. These are explicit construction conditions, not published hypotheses for the main result.

  1. def OAI.CoarseAssembly.fiberBlockEntry line 24
  2. theorem OAI.CoarseAssembly.spatialBlocks_entry line 39
  3. theorem OAI.CoarseAssembly.spatialBlocks_generator line 51
  4. theorem OAI.CoarseAssembly.spatialBlocks_intertwines line 94
  5. theorem OAI.CoarseAssembly.spatialBlocks_compression line 119