OAI/Combinatorics/ThinTrees/Signing/RealMatrixBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Real matrix bridge.

  1. def OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix line 16
  2. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_one line 19
  3. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_add line 22
  4. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_sub line 26
  5. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_smul line 30
  6. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_mul line 34
  7. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_transpose line 38
  8. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_hermitian line 42
  9. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_psd line 48
  10. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.of_complexMatrix_psd line 56
  11. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.complexMatrix_mono line 73
  12. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.of_complexMatrix_le line 78
  13. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.le_norm_identity line 84
  14. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.norm_le_of_psd_bound line 90
  15. lemma OAI.AlgorithmicThinTrees.RealMatrixBridge.bounds_of_norm_le line 98