OAI/Probability/SKGap/Matrix/ConditionalMiddleNorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.real_opNorm_add line 13
2. lemma OAI.SKGap.real_opNorm_smul line 18
3. lemma OAI.SKGap.operator_vecMulVec_le line 22
4. lemma OAI.SKGap.operator_mulVec_norm_le line 37
5. lemma OAI.SKGap.goeBilinear_norm_bound line 41
6. lemma OAI.SKGap.conditionalBlockMatrix_norm line 50