OAI/Probability/SKGap/Matrix/ConditionalEmpiricalNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.outer_symmetric line 13
2. lemma OAI.SKGap.outer_sum_symmetric line 18
3. lemma OAI.SKGap.conditionalBlockMatrix_hermitian line 23
4. lemma OAI.SKGap.empiricalConditionalMiddle_hermitian line 37
5. lemma OAI.SKGap.empiricalConditionalMiddle_norm line 46
6. lemma OAI.SKGap.scalarS_pos_of_time line 112
7. theorem OAI.SKGap.empiricalConditionalMiddle_uniform_norm line 117