OAI/Analysis/VlasovMaxwell/Retarded/MagneticMomentDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.contDiffOn_retardedMagneticDensity line 34
  2. lemma OAI.RVM.integrableOn_retardedMagneticDensity line 45
  3. def OAI.RVM.magneticMomentDensity line 73
  4. lemma OAI.RVM.integrableOn_magneticMomentDensity line 79
  5. lemma OAI.RVM.classical_retarded_magnetic_moment_identity line 93
  6. lemma OAI.RVM.magneticMomentDensity_actual line 139
  7. lemma OAI.RVM.integrated_magneticMomentDensity_actual line 176
  8. lemma OAI.RVM.classical_shifted_magnetic_physical_representation line 217