OAI/Analysis/VlasovMaxwell/LocalPDE/StrongLocalExistence.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.BoundedSpatiallySmoothSlab line 17
  2. lemma OAI.RVM.boundedSpatiallySmoothSlab_of_uniform_jets line 22
  3. theorem OAI.RVM.exists_local_spatially_smooth_bounded_classical line 38
  4. theorem OAI.RVM.exists_local_smooth_bounded_prefix line 87
  5. def OAI.RVM.timeSliceDatum line 160
  6. lemma OAI.RVM.SmoothClassicalPrefix.slice_admissible line 163
  7. structure OAI.RVM.DatumRestartControl line 182
  8. theorem OAI.RVM.family_global_picard_invariance line 195
  9. theorem OAI.RVM.family_picard_control line 269
  10. theorem OAI.RVM.family_contractive_picard_sequence line 418
  11. theorem OAI.RVM.family_picard_field_limit line 477
  12. theorem OAI.RVM.family_local_spatially_smooth_bounded_classical line 513
  13. def OAI.RVM.timePaste line 576
  14. lemma OAI.RVM.timePaste_left line 579
  15. lemma OAI.RVM.timePaste_right line 583
  16. lemma OAI.RVM.continuousOn_timePaste line 592
  17. lemma OAI.RVM.spatiallySmoothSlab_timePaste line 624
  18. lemma OAI.RVM.boundedSpatiallySmoothSlab_timePaste line 648
  19. lemma OAI.RVM.hasDerivWithinAt_timePaste line 664
  20. lemma OAI.RVM.slabTimeContinuousL2_timePaste line 704