OAI/Analysis/KadisonKastler/RectangularHilbert.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rectangular operator matrices on finite Hilbert sums

  1. def OAI.KadisonKastler.rectangularHilbertMatrix line 19
  2. theorem OAI.KadisonKastler.rectangularHilbertMatrix_apply line 27
  3. def OAI.KadisonKastler.hilbertExtendLeft line 32
  4. def OAI.KadisonKastler.hilbertExtendRight line 35
  5. def OAI.KadisonKastler.hilbertRestrictRight line 38
  6. theorem OAI.KadisonKastler.norm_hilbertExtendLeft line 43
  7. theorem OAI.KadisonKastler.norm_hilbertExtendRight line 49
  8. theorem OAI.KadisonKastler.norm_hilbertRestrictRight_le line 54
  9. theorem OAI.KadisonKastler.hilbertMatrix_rectangularCorner line 61
  10. theorem OAI.KadisonKastler.norm_rectangularHilbertMatrix line 71

    Source documentation

    The rectangular C⋆-matrix norm is its actual Hilbert-space operator norm.

    theorem norm_rectangularHilbertMatrix (M : CStarMatrix m n (H →L[ℂ] H)) :
    ‖rectangularHilbertMatrix M‖ = ‖M‖ := by
…

    Mentions: OAI.KadisonKastler.rectangularHilbertMatrix

  11. theorem OAI.KadisonKastler.norm_tupleSingle line 93
  12. theorem OAI.KadisonKastler.norm_hilbertTuple_coordinate_le line 100

    Source documentation

    Passing to one coordinate in each member of a Hilbert tuple is contractive.

    theorem norm_hilbertTuple_coordinate_le {W : Submodule ℂ (Generator.FiniteHilbert n H)}
    (i : n) (x : Generator.FiniteHilbert m W) :
    ‖WithLp.toLp 2 (fun j => ((x j : W) : Generator.FiniteHilbert n H) i)‖ ≤ ‖x‖ := by
…

    Mentions: OAI.Generator.FiniteHilbert