OAI/Topology/CoarseAssembly/HilbertSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Flattening the Hilbert sum of the finite fibers

The transfer is naturally constructed as a block operator. Flattening its Hilbert sum identifies it isometrically with the ordinary Roe module on the sigma type of vertices. Both directions and the norm identity are constructed from summability of squared norms.

  1. theorem OAI.CoarseAssembly.l2_norm_sq line 23
  2. theorem OAI.CoarseAssembly.l2_summable_sq line 28
  3. theorem OAI.CoarseAssembly.flattenVector_norm line 34
  4. def OAI.CoarseAssembly.flattenIsometry line 46
  5. theorem OAI.CoarseAssembly.flatten_unflatten line 54
  6. theorem OAI.CoarseAssembly.unflatten_flatten line 60