OAI/Analysis/KadisonKastler/HilbertDefect.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The defect isometry of a Hilbert-space contraction

The positive square root of 1 - A* A completes a contraction to an isometry. This is the geometric ingredient in finite block completion.

  1. def OAI.KadisonKastler.operatorDefect line 24
  2. theorem OAI.KadisonKastler.operatorDefect_selfadjoint line 27
  3. theorem OAI.KadisonKastler.adjoint_comp_self_le_one line 30
  4. theorem OAI.KadisonKastler.operatorDefect_sq line 38
  5. theorem OAI.KadisonKastler.norm_operatorDefect_sq line 42
  6. def OAI.KadisonKastler.defectIsometry line 55

    Source documentation

    The first component is the original contraction; the second accounts for exactly the lost squared norm.

    def defectIsometry (A : E →L[ℂ] F) (hA : ‖A‖ ≤ 1) :
    E →ₗᵢ[ℂ] WithLp 2 (F × E) where
…