OAI/Analysis/BiholderTransport/LinearAlgebra/ContactDifferential.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.exists_normal_local_inverse_at line 31
2. def OAI.WeakMTWTransport.normalHessianOperator line 62
3. lemma OAI.WeakMTWTransport.inner_normalHessianOperator line 71
4. lemma OAI.WeakMTWTransport.prefixNormalCost_source_hessian_full line 76
5. lemma OAI.WeakMTWTransport.normal_contact_twist line 96
6. lemma OAI.WeakMTWTransport.contact_selection_normal_differential line 121