OAI/Analysis/Kaplansky/Operators.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kaplansky.HilbertColumns line 15
2. def OAI.Kaplansky.operatorMatrixAction line 17
3. theorem OAI.Kaplansky.operatorMatrixAction_apply line 20
4. theorem OAI.Kaplansky.operatorMatrixAction_norm_le line 26
5. theorem OAI.Kaplansky.operatorMatrixAction_inner line 46

   Source documentation

   The rectangular matrix column identity implies a Hilbert-space isometry, with no finite-dimensional assumption on the Hilbert fibers.

   theorem operatorMatrixAction_inner (W : Fin m → Fin n → H →L[ℂ] H)
       (hW : ∀ i j, (∑ row, (W row i).adjoint.comp (W row j)) =
         if i=j then ContinuousLinearMap.id ℂ H else 0)
       (v w : HilbertColumns n H) :
       inner ℂ (operatorMatrixAction W v) (operatorMatrixAction W w)=inner ℂ v w := by
   …

   Mentions: OAI.Kaplansky.HilbertColumns, OAI.Kaplansky.operatorMatrixAction

6. theorem OAI.Kaplansky.operatorMatrixAction_norm line 68
7. theorem OAI.Kaplansky.operatorMatrixAction_sub line 85
8. theorem OAI.Kaplansky.operatorMatrix_perturbation_lower_bound line 94