OAI/Analysis/VlasovMaxwell/Regularity/SlabEvolutionRegularity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.differentiableWithinAt_slab_time line 17
  2. lemma OAI.RVM.C1ClassicalPrefix.hasDerivWithinAt_particle line 25
  3. lemma OAI.RVM.C1ClassicalPrefix.hasDerivWithinAt_electric line 40
  4. lemma OAI.RVM.C1ClassicalPrefix.hasDerivWithinAt_magnetic line 53
  5. lemma OAI.RVM.C1ClassicalPrefix.spatialJetRegular_all line 64
  6. lemma OAI.RVM.C1ClassicalPrefix.smooth line 79
  7. theorem OAI.RVM.exists_local_smooth_classical_prefix line 89
  8. lemma OAI.RVM.SmoothClassicalPrefix.toC1 line 104
  9. structure OAI.RVM.BoundedClassicalPrefix line 109
  10. lemma OAI.RVM.exists_bounded_classical_prefix line 116
  11. def OAI.RVM.pasteSolution line 121
  12. lemma OAI.RVM.slabRHS_congr line 124
  13. lemma OAI.RVM.pasteSolution_rhs line 141
  14. lemma OAI.RVM.spatiallySmooth_time_derivatives_smooth line 163
  15. lemma OAI.RVM.slabEquations_of_time_derivatives line 184
  16. lemma OAI.RVM.BoundedClassicalPrefix.paste line 207
  17. theorem OAI.RVM.BoundedClassicalPrefix.extend line 284