OAI/Analysis/BiholderTransport/Regularity/OuterTemplate.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.contDiff_primitive line 11
  2. def OAI.WeakMTWTransport.outerW line 19
  3. def OAI.WeakMTWTransport.outerJ line 23
  4. def OAI.WeakMTWTransport.outerProfile line 25
  5. lemma OAI.WeakMTWTransport.outerW_contDiff line 28
  6. lemma OAI.WeakMTWTransport.outerJ_contDiff line 34
  7. lemma OAI.WeakMTWTransport.outerProfile_contDiff line 37
  8. lemma OAI.WeakMTWTransport.outerJ_hasDerivAt line 42
  9. lemma OAI.WeakMTWTransport.outerW_zero_right line 47
  10. lemma OAI.WeakMTWTransport.outerW_nonneg line 54
  11. lemma OAI.WeakMTWTransport.outerJ_monotone line 66
  12. lemma OAI.WeakMTWTransport.outerW_affine line 73
  13. lemma OAI.WeakMTWTransport.outerProfile_left line 82
  14. lemma OAI.WeakMTWTransport.outerJ_zero line 88