OAI/Analysis/BiholderTransport/Regularity/StationaryPullback.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.second_fderiv_sub line 17
  2. lemma OAI.WeakMTWTransport.second_fderiv_const_mul line 30
  3. lemma OAI.WeakMTWTransport.second_fderiv_comp_stationary line 37
  4. def OAI.WeakMTWTransport.fixedJoinAction line 72
  5. def OAI.WeakMTWTransport.fixedJoinMiddle line 77
  6. lemma OAI.WeakMTWTransport.fixedJoinMiddle_apply line 91
  7. lemma OAI.WeakMTWTransport.fixedJoinAction_rescale line 96
  8. lemma OAI.WeakMTWTransport.fixedJoinMiddle_rescale line 107
  9. lemma OAI.WeakMTWTransport.fixedJoinAction_schur line 131