OAI/Analysis/InterpolatedFactors/MatrixNormal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.HilbertUltraweak.finset_sum_continuous line 14
  2. theorem OAI.FreeGroupFactorMain.Amplification.matrixEntry_normal line 29
  3. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_normal line 36
  4. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerEntry_normal line 43
  5. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerOfMatrix_normal line 54
  6. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerIso_normal line 72
  7. theorem OAI.FreeGroupFactorMain.Amplification.productSingle_norm line 92
  8. theorem OAI.FreeGroupFactorMain.Amplification.matrixBlock_productSingle line 99
  9. theorem OAI.FreeGroupFactorMain.Amplification.finiteDiagonal_productSingle line 104
  10. theorem OAI.FreeGroupFactorMain.Amplification.finiteProjection_trace line 124
  11. theorem OAI.FreeGroupFactorMain.Amplification.stabilizedTrace_matrix line 150
  12. theorem OAI.FreeGroupFactorMain.Amplification.finiteCorner_trace line 159
  13. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerIso_trace line 184