OAI/Topology/CoarseAssembly/UnitaryIndex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Unitary invariance of the explicit cycle index

  1. theorem OAI.CoarseAssembly.Analytic.operatorConjugation_equiv line 13
  2. theorem OAI.CoarseAssembly.Analytic.symmetricCutDown_map line 22
  3. theorem OAI.CoarseAssembly.Analytic.positiveProjection_map line 29
  4. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_map line 35
  5. theorem OAI.CoarseAssembly.Analytic.fredholmIndex_conjugation line 39
  6. theorem OAI.CoarseAssembly.Analytic.rawCycleToeplitz_unitary line 53
  7. theorem OAI.CoarseAssembly.Analytic.rawCycleIndex_unitary line 66