OAI/Analysis/BiholderTransport/LinearAlgebra/SchurCalculus.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.stationary_graph_hessian_identity line 19
2. lemma OAI.WeakMTWTransport.stationary_graph_envelope_fderiv line 41
3. lemma OAI.WeakMTWTransport.stationary_graph_schur_hessian line 52
4. lemma OAI.WeakMTWTransport.fixedSplitAction_contDiffAt line 105
5. lemma OAI.WeakMTWTransport.fixedSplitAction_source_hessian line 115
6. lemma OAI.WeakMTWTransport.exists_splitAction_schur_operator line 130