OAI/Analysis/VlasovMaxwell/Geometry/ParticleBySpacetime.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.integral_directional_derivative_zero line 13
  2. lemma OAI.RVM.integral_divergence_zero line 28
  3. lemma OAI.RVM.integral_mul_spatialPartial line 44
  4. lemma OAI.RVM.fderiv_q_apply line 57
  5. lemma OAI.RVM.spatialPartial_q line 71
  6. lemma OAI.RVM.contDiff_lorentz line 74
  7. lemma OAI.RVM.divergence_lorentz line 78
  8. lemma OAI.RVM.divergence_energy_lorentz line 86
  9. lemma OAI.RVM.integral_momentum_work line 105
  10. lemma OAI.RVM.hasFDerivAt_integral_uniform_support line 136
  11. lemma OAI.RVM.compactSupport_of_zero_off line 169
  12. lemma OAI.RVM.compactSupport_param_fderiv line 178
  13. lemma OAI.RVM.integrable_param_fderiv line 194
  14. lemma OAI.RVM.fderiv_integral_uniform_support_apply line 207
  15. lemma OAI.RVM.fderiv_weighted_param line 220
  16. lemma OAI.RVM.fderiv_weighted_integral_uniform_support_apply line 231
  17. lemma OAI.RVM.clm_spacetime_velocity_split line 250
  18. lemma OAI.RVM.fderiv_velocity_slice line 267
  19. lemma OAI.RVM.integrable_param_fderiv_apply_weight line 274
  20. lemma OAI.RVM.q_mul_velocity line 288
  21. lemma OAI.RVM.particle_energy_balance_param line 292
  22. def OAI.RVM.particleBySpacetime line 338
  23. lemma OAI.RVM.contDiff_reassociate line 341
  24. lemma OAI.RVM.particle_spacetime_local_data line 345
  25. lemma OAI.RVM.fderiv_particleBySpacetime line 364
  26. lemma OAI.RVM.particle_spacetime_vlasov line 381
  27. lemma OAI.RVM.classical_particle_energy_balance line 391
  28. lemma OAI.RVM.contDiffOn_integral_uniform_support line 401
  29. lemma OAI.RVM.integral_vec_apply line 419
  30. lemma OAI.RVM.param_moment_component line 423
  31. def OAI.RVM.particleEnergy line 437
  32. def OAI.RVM.particleFlux line 440
  33. def OAI.RVM.totalEnergy line 443
  34. def OAI.RVM.totalFlux line 446
  35. lemma OAI.RVM.classical_particle_energy_flux_regular line 449