feat: Start split of Distributional EM#1063
Conversation
zhikaip
left a comment
zhikaip
left a comment
There was a problem hiding this comment.
I think the framing should be that Distributions are "necessary", but not necessarily "better". it is needed to handles things properly but we shouldn't rely on it to do everything. (I'll keep looking for a way to do EM stuff the "engineering" or "undergraduate" way and hope we meet somewhere in the middle)
| are not smooth functions: point particles, infinitely thin wires, charged surfaces, and so on. | ||
| A point charge, for example, is conventionally written as `ρ(x) = q δ³(x - x₀)`, where `δ³` | ||
| is the Dirac delta. These idealisations are not functions in the usual sense, and cannot be | ||
| described within a formulation of electromagnetism that only allows smooth functions, because |
There was a problem hiding this comment.
I think "Cannot be described within a formulation of electromagnetism that only allows smooth functions" is too strong, I do want to build smooth version on the punctured space (which links to this), and this shouldn't be the only formulation in Physlib which forces us to always carry distributions around
There was a problem hiding this comment.
maybe be a bit explicit, something like "the fields of singular sources can be treated classically on the appropriate punctured domain, but the sources themselves and the differential form of Maxwell's equations including the singularity require distributions."
| mathematical object is called a tempered distribution. Fields and charge or current | ||
| distributions are then specified by their action on test functions rather than by their | ||
| pointwise values. Ordinary smooth functions `f` still fit into this framework via the rule | ||
| `φ ↦ ∫ f φ dx`, but the framework is strictly larger: it also accommodates point particles, |
There was a problem hiding this comment.
"the framework is strictly larger" is too strong as well, maybe some thing like "the framework accommodates objects that smooth functions cannot represent (point particles, surface charges, derivatives of step functions), at the cost of giving up pointwise values and pointwise products."
| distributions is not defined. For a point charge, for instance, both `A` and `J` are singular | ||
| at the location of the charge, and their product has no distributional meaning. | ||
|
|
||
| Other constructions must be reformulated rather than abandoned. The flux of `E` out of a |
There was a problem hiding this comment.
this section may be we can leave it for now, but I'd hope that after things are more fleshed out we can rewrite it to show how the distributional pairing relates to the functional API
|
@zhikaip Tried to rewrite to incorporate your comments here and other thoughts. |
2 participants
Added a Basic.lean file for Distributional EM with the idea that a future PR will move the distribution stuff to this file (I would add a TODO item here, however waiting for #1062). I'm hoping that this doc-string will help clarify what distributional EM is, and how e.g. the integral forms fit in.