OAI/Probability/SKGap/Matrix/RegularizedLogDet.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.LogDet.regularizedGram line 14
2. def OAI.SKGap.LogDet.regularizedLogDet line 16
3. lemma OAI.SKGap.LogDet.regularizedGram_posDef line 19
4. lemma OAI.SKGap.LogDet.regularizedGram_transpose line 24
5. lemma OAI.SKGap.LogDet.frobenius_sq_trace line 28
6. lemma OAI.SKGap.LogDet.trace_inner_abs line 34
7. lemma OAI.SKGap.LogDet.regularized_resolvent_square line 45
8. lemma OAI.SKGap.LogDet.regularized_resolvent_frobenius line 65
9. lemma OAI.SKGap.LogDet.hasDerivAt_regularizedGram line 75
10. lemma OAI.SKGap.LogDet.trace_regularized_derivative line 84
11. lemma OAI.SKGap.LogDet.hasDerivAt_regularizedLogDet line 96
12. lemma OAI.SKGap.LogDet.regularized_gradient_bound line 105
13. lemma OAI.SKGap.LogDet.regularized_derivative_bound line 117
14. theorem OAI.SKGap.LogDet.regularizedLogDet_lipschitz line 129
15. lemma OAI.SKGap.LogDet.logdet_le_trace_sub_card line 151
16. lemma OAI.SKGap.LogDet.regularized_factorization line 159
17. lemma OAI.SKGap.LogDet.regularizedLogDet_le_logdet line 168
18. lemma OAI.SKGap.LogDet.frobenius_le_sqrt_card_opNorm line 190
19. lemma OAI.SKGap.LogDet.regularizedLogDet_le_logdet_opNorm line 199
20. lemma OAI.SKGap.LogDet.regularizedLogDet_zero line 212
21. lemma OAI.SKGap.LogDet.regularizedLogDet_abs line 219