OAI/Probability/SKRatio/Matrices/RealPart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatioGaussian.RealComplex.realPart line 46
2. lemma OAI.SKRatioGaussian.RealComplex.norm_realPart_le line 48
3. lemma OAI.SKRatioGaussian.RealComplex.realPart_sub line 59
4. lemma OAI.SKRatioGaussian.RealComplex.realPart_liftMatrix line 62
5. lemma OAI.SKRatioGaussian.RealComplex.realPart_lipschitz line 65
6. lemma OAI.SKRatioGaussian.RealComplex.reVec_norm_le line 71
7. lemma OAI.SKRatioGaussian.RealComplex.realPart_operator line 75
8. lemma OAI.SKRatioGaussian.RealComplex.operator_realPart_le line 81
9. lemma OAI.SKRatioGaussian.RealComplex.liftMatrix_inverse line 87