OAI/Analysis/BiholderTransport/LinearAlgebra/HessianSmooth.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.hessianValue_contDiffAt line 110
2. lemma OAI.WeakMTWTransport.WeakMTW.transverse_concaveOn_injectivityDomain line 133
3. lemma OAI.WeakMTWTransport.iteratedDeriv_two_affine_line line 158
4. lemma OAI.WeakMTWTransport.directional_fderiv_hasDerivAt line 177
5. lemma OAI.WeakMTWTransport.positive_schur_test line 192
6. lemma OAI.WeakMTWTransport.nonzero_pairing_positive_test line 198