OAI/Probability/SKRatio/Matrices/LiftMatrix.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.RealComplex.liftMatrix line 46
2. abbrev OAI.SKRatioGaussian.RealComplex.clin line 47
3. abbrev OAI.SKRatioGaussian.RealComplex.rlin line 48
4. def OAI.SKRatioGaussian.RealComplex.reVec line 50
5. def OAI.SKRatioGaussian.RealComplex.imVec line 52
6. def OAI.SKRatioGaussian.RealComplex.liftVec line 54
7. lemma OAI.SKRatioGaussian.RealComplex.vec_norm_split line 58
8. lemma OAI.SKRatioGaussian.RealComplex.norm_liftVec line 70
9. lemma OAI.SKRatioGaussian.RealComplex.reVec_clin line 74
10. lemma OAI.SKRatioGaussian.RealComplex.imVec_clin line 80
11. lemma OAI.SKRatioGaussian.RealComplex.clin_liftVec line 86
12. lemma OAI.SKRatioGaussian.RealComplex.operator_norm_lift line 92
13. lemma OAI.SKRatioGaussian.RealComplex.norm_liftMatrix line 112
14. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_sub line 116
15. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_add line 119
16. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_mul line 122
17. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_one line 126
18. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_smul line 129
19. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_conjTranspose line 132
20. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_hermitian line 135
21. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_injective line 138