feat: Static EM

[jstoobysmith]

Implementing some useful definitions related to static electromagnetism, including the creation of a Lorentz current from a static charge density, and a EM 4-potential from a scalar potential.

Also introduce the notation mentioned here:

https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Normed.20dual.20of.20Schwarz.20space/near/573759094

which is used throughout.

[zhikaip]

Do you think electrostatics deserve its own file or even folder? I'm thinking that there's a difference between building an API for point charges for more complex problems and demonstrating the physics of a simple point charge, and I think we should actually separate those. The current PointParticle folder leans towards the latter.

I propose that we can do

Electrostatics
- PointParticle
- - OneDimension
- - ThreeDimension
- Current
- - ...
- Current and charges
- - ...

Then we have a collection of examples sitting nicely in one place. The general API for point charges can go elsewhere. What do you think about this? (I'm also experimenting with ways to refactor, if you think this is too much work, I don't mind merging this first and worrying about it later.)

[jstoobysmith]

I think this makes sense. Are we sure having a steady-state 'current' corresponds to electrostatics though? Not sure about the terminology here.

[zhikaip]

I think this makes sense. Are we sure having a steady-state 'current' corresponds to electrostatics though? Not sure about the terminology here.

I think you're right, for some reason I've always thought electrostatics and magnetostatics are the same thing, probably best to separate them.