OAI/Topology/CoarseAssembly/DirectSumIndex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Direct-sum additivity of the explicit cycle index

  1. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_cutDown line 13
  2. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_positive line 25
  3. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_toeplitz line 36
  4. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_unitaryExtension line 45
  5. theorem OAI.CoarseAssembly.Analytic.rawCycleToeplitz_directSum line 58
  6. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_coordinates line 66
  7. theorem OAI.CoarseAssembly.Analytic.rawCycleIndex_directSum line 79