OAI/Topology/CoarseAssembly/IsometryDilation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The explicit two-by-two dilation of a spatial isometry

  1. def OAI.CoarseAssembly.Analytic.isometryDilation line 15
  2. theorem OAI.CoarseAssembly.Analytic.isometryDilation_selfAdjoint line 18
  3. theorem OAI.CoarseAssembly.Analytic.isometry_complement_relations line 23
  4. theorem OAI.CoarseAssembly.Analytic.isometryDilation_sq line 37
  5. def OAI.CoarseAssembly.Analytic.isometryDilationPath line 54
  6. theorem OAI.CoarseAssembly.Analytic.isometryDilationPath_continuous line 59
  7. theorem OAI.CoarseAssembly.Analytic.isometryDilationPath_start line 62
  8. theorem OAI.CoarseAssembly.Analytic.isometryDilationPath_finish line 65
  9. theorem OAI.CoarseAssembly.Analytic.isometryDilation_conjugation line 70

    Source documentation

    Conjugating the stabilized operator gives its identity extension.

    theorem isometryDilation_conjugation (V a : A) (hV : star V * V = 1) :
    isometryDilation V * !![1, 0; 0, a] * isometryDilation V =
      !![1 + V * (a - 1) * star V, 0; 0, 1] := by
…

    Mentions: OAI.CoarseAssembly.Analytic.isometryDilation