OAI/Analysis/VlasovMaxwell/Flow/FlowDerivative.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.hasFDerivAt_variational_flow line 25
  2. lemma OAI.RVM.exists_local_differentiable_flow line 86
  3. def OAI.RVM.determinantMultilinear line 105
  4. lemma OAI.RVM.determinant_derivative line 110
  5. lemma OAI.RVM.determinant_row_mul_derivative line 123
  6. lemma OAI.RVM.determinant_variational_derivative line 133
  7. lemma OAI.RVM.determinant_eq_one_of_trace_zero line 139
  8. lemma OAI.RVM.determinant_retarded_rank_one line 167
  9. def OAI.RVM.endomorphismMatrix line 199
  10. lemma OAI.RVM.endomorphismMatrix_apply line 203
  11. lemma OAI.RVM.endomorphismMatrix_comp line 207
  12. lemma OAI.RVM.hasDerivAt_endomorphismMatrix line 212
  13. lemma OAI.RVM.determinant_clm_variational_derivative line 226
  14. lemma OAI.RVM.determinant_clm_eq_one_of_trace_zero line 239
  15. lemma OAI.RVM.flow_injOn_of_local_ode line 261
  16. lemma OAI.RVM.exists_local_volume_flow line 285
  17. lemma OAI.RVM.integral_image_volume_flow line 316
  18. lemma OAI.RVM.lintegral_image_volume_flow line 328