OAI/Probability/SKGap/Matrix/LiftMatrix.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.RealComplex.liftMatrix line 45
  2. abbrev OAI.SKGap.RealComplex.clin line 46
  3. abbrev OAI.SKGap.RealComplex.rlin line 47
  4. def OAI.SKGap.RealComplex.reVec line 49
  5. def OAI.SKGap.RealComplex.imVec line 51
  6. def OAI.SKGap.RealComplex.liftVec line 53
  7. lemma OAI.SKGap.RealComplex.vec_norm_split line 57
  8. lemma OAI.SKGap.RealComplex.norm_liftVec line 69
  9. lemma OAI.SKGap.RealComplex.reVec_clin line 73
  10. lemma OAI.SKGap.RealComplex.imVec_clin line 79
  11. lemma OAI.SKGap.RealComplex.clin_liftVec line 85
  12. lemma OAI.SKGap.RealComplex.operator_norm_lift line 91
  13. lemma OAI.SKGap.RealComplex.norm_liftMatrix line 111
  14. lemma OAI.SKGap.RealComplex.liftMatrix_sub line 115
  15. lemma OAI.SKGap.RealComplex.liftMatrix_add line 118
  16. lemma OAI.SKGap.RealComplex.liftMatrix_mul line 121
  17. lemma OAI.SKGap.RealComplex.liftMatrix_one line 125
  18. lemma OAI.SKGap.RealComplex.liftMatrix_smul line 128
  19. lemma OAI.SKGap.RealComplex.liftMatrix_conjTranspose line 131
  20. lemma OAI.SKGap.RealComplex.liftMatrix_hermitian line 134
  21. lemma OAI.SKGap.RealComplex.liftMatrix_injective line 137