OAI/Topology/CoarseAssembly/FiniteCycleSum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite active sums of analytic cycles

Countably many summands are allowed as an ambient Hilbert space; all but finitely many cycles are degenerate. The finite active length may later vary with the component of the coarse disjoint union.

  1. theorem OAI.CoarseAssembly.Analytic.diagonal_compact_of_zero_tail line 19
  2. abbrev OAI.CoarseAssembly.Analytic.familyHilbert line 46
  3. def OAI.CoarseAssembly.Analytic.familyRepresentation line 48
  4. theorem OAI.CoarseAssembly.Analytic.familyRepresentation_apply line 83
  5. def OAI.CoarseAssembly.Analytic.finiteActiveCycle line 87
  6. theorem OAI.CoarseAssembly.Analytic.finiteActiveCycle_unital line 120
  7. theorem OAI.CoarseAssembly.Analytic.finiteActiveCycle_selfAdjoint line 134
  8. theorem OAI.CoarseAssembly.Analytic.finiteActiveCycle_norm line 145