OAI/Topology/CoarseAssembly/BoundedTransformCompact.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The bounded transform changes a unital Fredholm operator compactly

  1. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_normSquare line 13
  2. theorem OAI.CoarseAssembly.Analytic.cayleyUnitary_mul_normSquare line 21
  3. theorem OAI.CoarseAssembly.Analytic.star_cayleyUnitary_mul_normSquare line 32
  4. theorem OAI.CoarseAssembly.Analytic.boundedTransform_mul_normSquare line 48
  5. theorem OAI.CoarseAssembly.Analytic.boundedTransform_eq_of_involution line 67
  6. theorem OAI.CoarseAssembly.Analytic.boundedTransform_sub_compact line 77