OAI/Probability/SpanningForest/ProjectionLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.ProjectionLimit.cycle_projection_tendsto line 15
2. theorem OAI.Problem336.ProjectionLimit.free_kernel_tendsto line 23
3. theorem OAI.Problem336.ProjectionLimit.kernel_matrix_tendsto line 32
4. theorem OAI.Problem336.ProjectionLimit.kernel_minor_tendsto line 44
5. theorem OAI.Problem336.ProjectionLimit.free_kernel_minor_tendsto line 53
6. theorem OAI.Problem336.ProjectionLimit.free_kernel_minor_ofReal_tendsto line 67
7. theorem OAI.Problem336.ProjectionLimit.projection_kernel_eq_gram line 82
8. theorem OAI.Problem336.ProjectionLimit.projection_kernel_minor_nonneg line 93