OAI/Probability/SpanningForest/FiniteKernelBridge.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem336.FiniteKernelBridge.embedding_rangeline 11 - theorem
OAI.Problem336.FiniteKernelBridge.embedding_projectionline 26 - theorem
OAI.Problem336.FiniteKernelBridge.transfer_entry_eq_finiteKernelline 31 - theorem
OAI.Problem336.FiniteKernelBridge.transfer_operator_eq_finiteKernelline 40 - theorem
OAI.Problem336.FiniteKernelBridge.transfer_minor_eq_finiteKernelline 50