OAI/Analysis/BiholderTransport/Calculus/JetPullback.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.second_fderiv_comp_affine line 17
2. lemma OAI.WeakMTWTransport.hasSecondTaylor_shift line 38
3. lemma OAI.WeakMTWTransport.half_norm_sq_hasFDerivAt line 66
4. lemma OAI.WeakMTWTransport.half_norm_sq_fderiv line 76
5. lemma OAI.WeakMTWTransport.half_norm_sq_second_fderiv line 81
6. lemma OAI.WeakMTWTransport.half_norm_sq_contDiff line 87
7. lemma OAI.WeakMTWTransport.norm_square_hasSecondTaylor line 91