OAI/Analysis/VlasovMaxwell/LocalPDE/EquationsBefore.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.EquationsBefore line 35
  2. def OAI.RVM.ClassicalBefore line 48
  3. lemma OAI.RVM.particle_spacetime_vlasov_before line 57
  4. lemma OAI.RVM.classical_retarded_electric_integral_identity_before line 67
  5. lemma OAI.RVM.classical_retarded_magnetic_integral_identity_before line 109
  6. lemma OAI.RVM.classical_retarded_electric_moment_identity_before line 157
  7. lemma OAI.RVM.classical_retarded_magnetic_moment_identity_before line 193
  8. lemma OAI.RVM.classical_positiveTimeShift_maxwell_before line 239
  9. lemma OAI.RVM.classical_shifted_electric_potential_representation_before line 276
  10. lemma OAI.RVM.classical_shifted_magnetic_potential_representation_before line 296
  11. lemma OAI.RVM.contDiff_shifted_moments_before line 314
  12. lemma OAI.RVM.ClassicalBefore.regularParticle line 320
  13. lemma OAI.RVM.electricMomentDensity_actual_before line 323
  14. lemma OAI.RVM.integrated_electricMomentDensity_actual_before line 362
  15. lemma OAI.RVM.classical_shifted_electric_physical_representation_before line 405
  16. lemma OAI.RVM.magneticMomentDensity_actual_before line 432
  17. lemma OAI.RVM.integrated_magneticMomentDensity_actual_before line 469
  18. lemma OAI.RVM.classical_shifted_magnetic_physical_representation_before line 510
  19. lemma OAI.RVM.continuousOn_electricConeBoundary_before line 533
  20. lemma OAI.RVM.continuousOn_magneticConeBoundary_before line 559
  21. lemma OAI.RVM.classical_electric_physical_representation_before line 581
  22. lemma OAI.RVM.classical_magnetic_physical_representation_before line 603
  23. lemma OAI.RVM.classical_electric_physical_vector_before line 625
  24. lemma OAI.RVM.classical_magnetic_physical_vector_before line 637
  25. lemma OAI.RVM.classical_physical_force_representation_before line 649
  26. lemma OAI.RVM.classical_electricConeBoundary_datum_before line 670
  27. lemma OAI.RVM.classical_magneticConeBoundary_datum_before line 676
  28. lemma OAI.RVM.ClassicalBefore.energyPrefix line 682
  29. lemma OAI.RVM.classical_boundaryLorentzForce_datum_before line 700
  30. lemma OAI.RVM.classical_retarded_force_representation_before line 711
  31. lemma OAI.RVM.classical_retarded_force_phase_integral_before line 726
  32. lemma OAI.RVM.classical_retarded_force_phase_domain_before line 737
  33. lemma OAI.RVM.classical_retarded_force_label_integral_before line 746