OAI/Analysis/VlasovMaxwell/Geometry/ShiftedRho.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.RegularParticle.time_moment_derivative line 35
  2. lemma OAI.RVM.RegularParticle.time_moment_integrable line 46
  3. lemma OAI.RVM.RegularParticle.scalar_moment_integrable line 53
  4. lemma OAI.RVM.current_eq_integral_component line 58
  5. lemma OAI.RVM.dirD_rho line 65
  6. lemma OAI.RVM.dirD_current_component line 70
  7. lemma OAI.RVM.classical_retarded_electric_moment_identity line 82
  8. def OAI.RVM.shiftedRho line 118
  9. def OAI.RVM.shiftedCurrent line 120
  10. def OAI.RVM.electricMomentDensity line 122
  11. lemma OAI.RVM.integrableOn_electricMomentDensity line 127
  12. lemma OAI.RVM.contDiff_shifted_moments line 136
  13. lemma OAI.RVM.retardedElectricDensity_component line 142
  14. lemma OAI.RVM.coneDirection_add line 164
  15. lemma OAI.RVM.electricMomentDensity_actual line 168
  16. lemma OAI.RVM.integrated_electricMomentDensity_actual line 207
  17. lemma OAI.RVM.classical_shifted_electric_physical_representation line 250