OAI/Analysis/VlasovMaxwell/Flow/LorentzPhase.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.trace_prod_diagonal line 23
  2. lemma OAI.RVM.trace_fderiv_eq_divergence line 40
  3. def OAI.RVM.lorentzPhase line 55
  4. lemma OAI.RVM.contDiff_lorentzPhase line 58
  5. lemma OAI.RVM.trace_lorentzPhase line 64
  6. lemma OAI.RVM.exists_bounded_ode_on_Icc line 97
  7. def OAI.RVM.cutLorentz line 127
  8. lemma OAI.RVM.cutLorentz_regular line 130
  9. lemma OAI.RVM.cutLorentz_bounded line 146
  10. lemma OAI.RVM.exists_characteristic_on_slab line 179
  11. theorem OAI.RVM.classical_initial_label line 214
  12. theorem OAI.RVM.classical_particle_bound line 229