OAI/Analysis/BiholderTransport/Regularity/ShortForward.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakMTWTransport.shortForward line 20
  2. def OAI.WeakMTWTransport.shortEnergy line 23
  3. lemma OAI.WeakMTWTransport.shortEnergy_eq_norm line 30
  4. lemma OAI.WeakMTWTransport.shortForward_zero line 43
  5. lemma OAI.WeakMTWTransport.shortForward_action line 49
  6. def OAI.WeakMTWTransport.parametricShortForward line 81
  7. def OAI.WeakMTWTransport.parametricShortEnergy line 84
  8. lemma OAI.WeakMTWTransport.parametricShortEnergy_contDiffAt line 89
  9. lemma OAI.WeakMTWTransport.parametricShortForward_contDiffAt line 100
  10. lemma OAI.WeakMTWTransport.parametricShortForward_regular_near line 124
  11. lemma OAI.WeakMTWTransport.geometric_parametric_short_family line 155