OAI/Probability/SKGap/Matrix/RankNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.real_eigenvalue_abs_le_opNorm line 12
2. lemma OAI.SKGap.frobenius_sq_le_rank_opNorm_sq line 22
3. lemma OAI.SKGap.frobenius_le_sqrt_rank_opNorm line 42
4. lemma OAI.SKGap.logdet_cube_difference line 59
5. lemma OAI.SKGap.logdet_cube_net_transfer line 74
6. lemma OAI.SKGap.logdet_rank_perturbation line 94
7. lemma OAI.SKGap.product_mesh_absorption line 106