OAI/Analysis/BiholderTransport/LinearAlgebra/CompactQuadratic.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.reverseRay_prefix line 52
  2. lemma OAI.WeakMTWTransport.proper_prefix_reverse_in_injectivityDomain line 56
  3. lemma OAI.WeakMTWTransport.proper_prefix_reverse_endpoint line 64
  4. def OAI.WeakMTWTransport.middleHessian line 70
  5. lemma OAI.WeakMTWTransport.middleHessian_apply line 77
  6. def OAI.WeakMTWTransport.middleCenteredAction line 86
  7. lemma OAI.WeakMTWTransport.middle_normal_prefix line 93
  8. lemma OAI.WeakMTWTransport.middle_normal_suffix line 100
  9. lemma OAI.WeakMTWTransport.middle_action_contact line 107
  10. lemma OAI.WeakMTWTransport.middleCenteredAction_minimum line 117
  11. lemma OAI.WeakMTWTransport.middleCenteredAction_contDiffAt line 133
  12. lemma OAI.WeakMTWTransport.middleCenteredAction_hessian line 145
  13. lemma OAI.WeakMTWTransport.middleHessian_one_nonneg line 159