OAI/Probability/SpanningForest/DeterminantalResponse.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.Determinantal.transferKernel line 14
2. theorem OAI.Problem336.Determinantal.transferKernel_transpose line 18
3. theorem OAI.Problem336.Determinantal.transferKernel_idempotent line 25
4. theorem OAI.Problem336.Determinantal.projection_diagonal_eq_sum_sq line 38
5. theorem OAI.Problem336.Determinantal.projection_diagonal_mem_Icc line 48
6. theorem OAI.Problem336.Determinantal.transferKernel_diagonal_mem_Icc line 64
7. def OAI.Problem336.Determinantal.pairMatrix line 70
8. theorem OAI.Problem336.Determinantal.pairMatrix_det line 74
9. theorem OAI.Problem336.Determinantal.determinantal_pair_covariance line 78
10. theorem OAI.Problem336.Determinantal.determinantal_pair_covariance_nonpos line 86