OAI/Probability/SKGap/Localization/ConditionalRankAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.conditionalColumns line 15
2. def OAI.SKGap.conditionalCoupling line 18
3. def OAI.SKGap.conditionalCoefficient line 20
4. lemma OAI.SKGap.conditionalCoefficient_hermitian line 25
5. lemma OAI.SKGap.conditional_rank_expansion line 34
6. lemma OAI.SKGap.conditional_schur_coefficient line 44
7. lemma OAI.SKGap.conditionalCoefficient_at_equality line 57
8. theorem OAI.SKGap.conditional_rank_change_basis line 71
9. theorem OAI.SKGap.compact_conditional_rank_criterion line 97
10. lemma OAI.SKGap.quadratic_lift_real line 144
11. lemma OAI.SKGap.complex_lowerRayleigh_margin line 149
12. theorem OAI.SKGap.bilinearPathGood_margin line 172