OAI/Analysis/KadisonKastler/RectangularOperator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Adjoint and product formulas for rectangular operator matrices

  1. theorem OAI.KadisonKastler.rectangularHilbertMatrix_mul line 21
  2. theorem OAI.KadisonKastler.rectangularHilbertMatrix_conjTranspose line 30
  3. theorem OAI.KadisonKastler.norm_rectangular_star line 41
  4. theorem OAI.KadisonKastler.norm_rectangular_mul_star line 45
  5. theorem OAI.KadisonKastler.norm_rectangular_star_apply_of_projection line 55

    Source documentation

    The adjoint of a partial isometry has the same norm on a vector as its range projection.

    theorem norm_rectangular_star_apply_of_projection [DecidableEq m]
    (V : CStarMatrix m n (H →L[ℂ] H))
    (hV : IsStarProjection (V * V.conjTranspose)) (z : Generator.FiniteHilbert m H) :
    ‖rectangularHilbertMatrix V.conjTranspose z‖ = ‖rectangularHilbertMatrix (V * V.conjTranspose) z‖ := by
…

    Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.rectangularHilbertMatrix