OAI/Analysis/VlasovMaxwell/Flow/ExtendedLorentz.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.exists_local_retarded_branch line 13
  2. lemma OAI.RVM.derivative_retarded_branch line 46
  3. lemma OAI.RVM.exists_local_retarded_branch_with_derivative line 66
  4. lemma OAI.RVM.hasDerivAt_cone_direction line 88
  5. lemma OAI.RVM.hasDerivAt_particle_energy line 108
  6. lemma OAI.RVM.hasDerivAt_particle_velocity line 119
  7. lemma OAI.RVM.dot_cross_self_left line 130
  8. lemma OAI.RVM.hasDerivAt_lorentz_energy line 134
  9. lemma OAI.RVM.contDiff_q line 139
  10. lemma OAI.RVM.contDiff_velocity line 143
  11. lemma OAI.RVM.contDiff_cross line 146
  12. def OAI.RVM.extendedLorentz line 157
  13. lemma OAI.RVM.contDiffAt_extendedLorentz line 160
  14. lemma OAI.RVM.exists_local_characteristic line 174
  15. lemma OAI.RVM.sum_basis line 203
  16. lemma OAI.RVM.clm_sum_basis line 207
  17. lemma OAI.RVM.full_directional_derivative line 212
  18. lemma OAI.RVM.hasDerivAt_particle_along_curve line 248
  19. lemma OAI.RVM.particle_differentiableAt_positive line 259
  20. lemma OAI.RVM.hasDerivAt_transport_zero line 271
  21. lemma OAI.RVM.transport_on_characteristic line 282
  22. lemma OAI.RVM.dot_cross_cycle line 302
  23. lemma OAI.RVM.cross_antisymm line 306
  24. lemma OAI.RVM.cross_dot_square line 310
  25. lemma OAI.RVM.norm_cross_le line 315
  26. lemma OAI.RVM.poynting_norm_le_energy line 321
  27. lemma OAI.RVM.field_cone_energy_identity line 326
  28. lemma OAI.RVM.good_field_square_le_flux line 338
  29. lemma OAI.RVM.fderiv_velocity_apply line 344
  30. lemma OAI.RVM.spatialPartial_velocity line 359
  31. lemma OAI.RVM.spatialPartial_mul line 371
  32. lemma OAI.RVM.spatialPartial_sub line 379
  33. lemma OAI.RVM.divergence_magnetic_force line 387
  34. lemma OAI.RVM.divergence_cross line 401
  35. lemma OAI.RVM.hasDerivAt_field_energy line 424
  36. lemma OAI.RVM.maxwell_energy_balance line 432