OAI/Analysis/VlasovMaxwell/Regularity/PositiveExtension.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.positiveTimeCut line 37
  2. def OAI.RVM.positiveTimeExtend line 38
  3. def OAI.RVM.positiveTimeShift line 41
  4. lemma OAI.RVM.contDiff_positiveTimeCut line 44
  5. lemma OAI.RVM.positiveTimeCut_zero line 46
  6. lemma OAI.RVM.positiveTimeCut_one line 48
  7. lemma OAI.RVM.contDiff_positiveTimeExtend line 53
  8. lemma OAI.RVM.positiveTimeExtend_eventually_eq line 67
  9. lemma OAI.RVM.contDiff_positiveTimeShift line 72
  10. lemma OAI.RVM.positiveTimeShift_eq line 77
  11. lemma OAI.RVM.fderiv_positiveTimeShift line 82
  12. lemma OAI.RVM.SmoothOnFiniteHorizons.field_positive line 97
  13. lemma OAI.RVM.SmoothOnFiniteHorizons.particle_positive line 106
  14. lemma OAI.RVM.SmoothOnFiniteHorizons.moments_positive line 113
  15. lemma OAI.RVM.spaceCurl_positiveTimeShift line 139
  16. lemma OAI.RVM.classical_positiveTimeShift_maxwell line 147
  17. lemma OAI.RVM.classical_shifted_electric_potential_representation line 184
  18. lemma OAI.RVM.classical_shifted_magnetic_potential_representation line 204