OAI/Topology/CoarseAssembly/CayleyBoundary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A rational representative of the odd analytic boundary

For a self-adjoint F, the square of its Cayley transform, with a minus sign, equals one modulo the square defect F² - 1. This construction will be applied to the Roe ideal in the controlled pseudolocal algebra.

  1. theorem OAI.CoarseAssembly.Analytic.selfAdjoint_add_I_isUnit line 22
  2. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_val line 33
  3. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_star line 37
  4. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_normal line 43
  5. theorem OAI.CoarseAssembly.Analytic.cayleyUnitary_val line 50
  6. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_defect line 54
  7. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_sub_one_mem line 75
  8. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_eq_one line 86