OAI/Analysis/VlasovMaxwell/Flow/HighFlow.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.iteratedFDeriv_id_high line 24
  2. lemma OAI.RVM.tame_flow_iteratedFDeriv line 30
  3. def OAI.RVM.SpatialJetBound line 96
  4. def OAI.RVM.lorentzNonlinearity line 101
  5. lemma OAI.RVM.lorentzNonlinearity_smooth line 104
  6. def OAI.RVM.lorentzArgument line 108
  7. lemma OAI.RVM.lorentzArgument_smooth line 111
  8. lemma OAI.RVM.lorentzArgument_derivative_le line 115
  9. lemma OAI.RVM.lorentzArgument_mem line 130
  10. lemma OAI.RVM.lorentzField_derivatives_bound line 136
  11. lemma OAI.RVM.lorentzField_derivative_tame line 162
  12. lemma OAI.RVM.flow_first_derivative_bound line 200
  13. lemma OAI.RVM.flow_derivatives_bound line 251
  14. lemma OAI.RVM.SmoothLorentzFlow.reversePath_smooth line 292
  15. lemma OAI.RVM.SmoothLorentzFlow.reversePath_integral line 297
  16. lemma OAI.RVM.SmoothLorentzFlow.reversePath_derivatives_bound line 309
  17. lemma OAI.RVM.SmoothLorentzFlow.backward_derivative_tame line 332