OAI/Analysis/BiholderTransport/Calculus/SecondTaylorComposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.HasSecondTaylor.diagonal_unique line 16
2. lemma OAI.WeakMTWTransport.HasSecondTaylor.congr_of_eventuallyEq line 28
3. lemma OAI.WeakMTWTransport.HasQuadraticExpansion.hasSecondTaylor' line 36
4. lemma OAI.WeakMTWTransport.quadratic_expansion_comp_proxy line 46
5. lemma OAI.WeakMTWTransport.quadratic_proxy_pullback line 65