From 976a2cddb2daae09283ffb15b50263bd14525838 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 28 Apr 2026 14:30:21 +0100 Subject: [PATCH 1/5] feat: Create Distributional.Basic --- .../Distributional/Basic.lean | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 Physlib/Electromagnetism/Distributional/Basic.lean diff --git a/Physlib/Electromagnetism/Distributional/Basic.lean b/Physlib/Electromagnetism/Distributional/Basic.lean new file mode 100644 index 000000000..f1ad032b0 --- /dev/null +++ b/Physlib/Electromagnetism/Distributional/Basic.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.SpaceAndTime.SpaceTime.Derivatives +public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv +/-! + +# Distributional Electromagnetic Potential + +## i. Overview + +In electromagnetism, charge and current distributions are often idealised as objects that +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 +they are incompatible with the assumption that a field has a well-defined value at every +point. The same issue arises for the fields they source: the electric field of a point charge +diverges at the location of the charge, and the magnetic field of an infinitely thin wire +diverges along the wire. + +The resolution is to give up asking for the value of a field +at a single point and instead ask for its value averaged over a region of space, weighted by +a test function `φ`. Physically, one can think of `φ` as the response profile of a measuring +device: a real device cannot probe a single mathematical point, but only a small region with +some smooth sensitivity profile. The idealised pointwise value is then replaced by the +weighted average `∫ f(x) φ(x) dx`, and a "field" is identified with the rule `φ ↦ ∫ f φ dx` +that sends each test function to a number. + +When the test functions are taken to be `Schwartz maps` (smooth functions which, together +with all their derivatives, decay faster than any polynomial at infinity), the resulting +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, +surface charges, and other singular sources. + +For example, if the charge distribution is represented by the tempered distribution `ρ`, then +the charge registered by a device with weighting `φ` is `ρ φ`, or notionally `∫ ρ(x) φ(x) dx`. +For a point charge `q` at the origin this evaluates to `q · φ(0)`: the device "sees" the +charge weighted by the value of its response profile at the location of the charge, exactly as +physical intuition would suggest. + +Derivatives still make sense in this framework, but they are defined by integration by parts. +If `f` is a tempered distribution, its derivative `∂f` is the distribution acting on test +functions by `(∂f) φ := - f (∂φ)`. For smooth `f` this reproduces the ordinary derivative +(the boundary terms vanish because Schwartz functions decay rapidly), but it also assigns a +meaningful derivative to objects such as the step function, whose distributional derivative +is the Dirac delta. This is what allows Maxwell's equations to retain their differential form +even when the sources are singular. + +Because pointwise values are no longer available, some constructions from classical +electromagnetism cease to be well defined in the distributional setting. The Lagrangian +density `ℒ = - Aᵤ Jᵘ - ¼ Fᵤᵥ Fᵘᵛ` is one such example: it relies on pointwise products of +distributions (such as `A` with `J`, or `F` with itself), and in general the product of two +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 +surface `S`, classically `∫_S E · dA`, is no longer well defined, but one can still speak of +the flux weighted by a test function `φ`, notionally defined as `- ∫ E x · ∇ φ x dx`. +Heuristically this comes from the divergence theorem: if `φ` were the indicator function +of the region enclosed by `S`, then `- ∇ φ` would be a delta function supported on `S` +pointing outward, recovering the surface integral. As `φ` approaches such an indicator +function (equal to `1` inside and `0` outside), this weighted flux approaches the flux +through `S`. The flux through `S` itself remains inaccessible inside the framework, since the +indicator function is not a Schwartz map; but it can be recovered as a limit of weighted +fluxes over progressively sharper test functions. + +In this setting, Gauss's law states precisely that the flux with weighting +`φ` equals the charge measured with the same weighting `φ`. Notionally this is +`- ∫ E x · ∇ φ x dx = ∫ ρ x φ x dx`. +In the distributional setting, this 'integral' form of Gauss's law +is exactly equivalent to the differential form `∇ · E = ρ`, +due to the way derivatives are defined by integration by parts. + +-/ From 8c34a6edd22e276d4ceb9fccdec35f3afde8edd7 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 28 Apr 2026 14:31:06 +0100 Subject: [PATCH 2/5] Update Physlib.lean --- Physlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Physlib.lean b/Physlib.lean index bcb7d0759..537f90be8 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -27,6 +27,7 @@ public import Physlib.Electromagnetism.Basic public import Physlib.Electromagnetism.Charge.ChargeUnit public import Physlib.Electromagnetism.Current.CircularCoil public import Physlib.Electromagnetism.Current.InfiniteWire +public import Physlib.Electromagnetism.Distributional.Basic public import Physlib.Electromagnetism.Dynamics.Basic public import Physlib.Electromagnetism.Dynamics.CurrentDensity public import Physlib.Electromagnetism.Dynamics.Hamiltonian From 619082bb1b0b0769fe4dd5cd44fb224baae72dda Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 28 Apr 2026 14:45:42 +0100 Subject: [PATCH 3/5] refactor: Update flux --- .../Electromagnetism/Distributional/Basic.lean | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/Physlib/Electromagnetism/Distributional/Basic.lean b/Physlib/Electromagnetism/Distributional/Basic.lean index f1ad032b0..0e2108237 100644 --- a/Physlib/Electromagnetism/Distributional/Basic.lean +++ b/Physlib/Electromagnetism/Distributional/Basic.lean @@ -63,13 +63,17 @@ 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 surface `S`, classically `∫_S E · dA`, is no longer well defined, but one can still speak of the flux weighted by a test function `φ`, notionally defined as `- ∫ E x · ∇ φ x dx`. -Heuristically this comes from the divergence theorem: if `φ` were the indicator function -of the region enclosed by `S`, then `- ∇ φ` would be a delta function supported on `S` -pointing outward, recovering the surface integral. As `φ` approaches such an indicator -function (equal to `1` inside and `0` outside), this weighted flux approaches the flux -through `S`. The flux through `S` itself remains inaccessible inside the framework, since the -indicator function is not a Schwartz map; but it can be recovered as a limit of weighted -fluxes over progressively sharper test functions. +The intuition is that `φ` plays the role of a smoothed-out version of the region `V` +enclosed by `S`: imagine `φ` equal to `1` deep inside `V`, equal to `0` far outside, and +transitioning smoothly across `S` over a thin layer. Its gradient `∇ φ` is then nonzero only +in this transition layer, points inward (from `0` to `1`), and concentrates more sharply on +`S` the thinner the layer is made. By the divergence theorem, +`- ∫ E · ∇ φ dV = ∫ φ (∇ · E) dV`, which for a sharp `φ` is approximately the integral of +`∇ · E` over `V`, i.e. the flux of `E` out of `S`. As `φ` is taken to be a sharper and sharper +approximation of `V`, the weighted flux approaches the classical flux through `S`. The flux +through `S` itself is not directly accessible in the framework, since a perfectly sharp `φ` +(equal to `1` on `V` and `0` outside, with no smooth transition) is not a Schwartz map; but +it can be recovered as a limit of weighted fluxes over progressively sharper test functions. In this setting, Gauss's law states precisely that the flux with weighting `φ` equals the charge measured with the same weighting `φ`. Notionally this is From 05e00dda6e811b43db1a19574ff6355d714e5317 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 28 Apr 2026 15:33:29 +0100 Subject: [PATCH 4/5] =?UTF-8?q?refactor:=20Add=20missing=20=CE=B5=E2=82=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Physlib/Electromagnetism/Distributional/Basic.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Physlib/Electromagnetism/Distributional/Basic.lean b/Physlib/Electromagnetism/Distributional/Basic.lean index 0e2108237..1de0d9296 100644 --- a/Physlib/Electromagnetism/Distributional/Basic.lean +++ b/Physlib/Electromagnetism/Distributional/Basic.lean @@ -76,10 +76,11 @@ through `S` itself is not directly accessible in the framework, since a perfectl it can be recovered as a limit of weighted fluxes over progressively sharper test functions. In this setting, Gauss's law states precisely that the flux with weighting -`φ` equals the charge measured with the same weighting `φ`. Notionally this is -`- ∫ E x · ∇ φ x dx = ∫ ρ x φ x dx`. +`φ` equals the charge measured with the same weighting `φ` (with +an additional factor of `1/ε₀`). Notionally this is +`- ∫ E x · ∇ φ x dx = ∫ ρ x φ x dx / ε₀`. In the distributional setting, this 'integral' form of Gauss's law -is exactly equivalent to the differential form `∇ · E = ρ`, +is exactly equivalent to the differential form `∇ · E = ρ / ε₀`, due to the way derivatives are defined by integration by parts. -/ From 325d901addfa36d4196ab76f0df1b90160945203 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 29 Apr 2026 09:59:20 +0100 Subject: [PATCH 5/5] refactor: wording --- .../Distributional/Basic.lean | 139 ++++++++++-------- 1 file changed, 77 insertions(+), 62 deletions(-) diff --git a/Physlib/Electromagnetism/Distributional/Basic.lean b/Physlib/Electromagnetism/Distributional/Basic.lean index 1de0d9296..4cfcd5076 100644 --- a/Physlib/Electromagnetism/Distributional/Basic.lean +++ b/Physlib/Electromagnetism/Distributional/Basic.lean @@ -13,74 +13,89 @@ public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv ## i. Overview -In electromagnetism, charge and current distributions are often idealised as objects that -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 -they are incompatible with the assumption that a field has a well-defined value at every -point. The same issue arises for the fields they source: the electric field of a point charge -diverges at the location of the charge, and the magnetic field of an infinitely thin wire -diverges along the wire. +In electromagnetism, charge and current distributions are often idealised as objects +such as point particles, infinitely thin wires, and charged surfaces. These idealisations +are not compatible with the usual demand that physical quantities be specified by a +well-defined value at each point in space: a point charge, for instance, has no finite +value at its location, and the field it sources diverges there. -The resolution is to give up asking for the value of a field -at a single point and instead ask for its value averaged over a region of space, weighted by -a test function `φ`. Physically, one can think of `φ` as the response profile of a measuring -device: a real device cannot probe a single mathematical point, but only a small region with -some smooth sensitivity profile. The idealised pointwise value is then replaced by the -weighted average `∫ f(x) φ(x) dx`, and a "field" is identified with the rule `φ ↦ ∫ f φ dx` -that sends each test function to a number. +One way to deal with this is to smear out the idealised objects themselves, replacing a +point charge by a narrow Gaussian distribution and so on. The approach adopted in this +module abandons the premise that physical quantities are defined by +their pointwise values at all. From the point of view of physics this costs nothing, since +no real measuring device probes a single mathematical point; every device has some finite +spatial extent and some smooth response profile across that extent. The most one can ask of +a physical quantity is that it return a well-defined reading for each such response +profile, and that the assignment satisfy two basic conditions: linearity, expressing that +combining two response profiles into a single device adds the readings, and continuity, +expressing that a small change to the response profile produces only a small change to the +reading. Taking the response profiles to be Schwartz maps — smooth functions which, +together with all their derivatives, decay faster than any polynomial at infinity — yields +the mathematical object that captures this picture: a *tempered distribution*, a +continuous linear map sending each Schwartz map to a number, vector, or similar value. -When the test functions are taken to be `Schwartz maps` (smooth functions which, together -with all their derivatives, decay faster than any polynomial at infinity), the resulting -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, -surface charges, and other singular sources. +The simplest tempered distributions are those associated with ordinary smooth functions. +A smooth function `f` defines the distribution `φ ↦ ∫ f x * φ x dx`, the weighted average +of `f` against the response profile `φ`. This rule is no longer indexed by the pointwise +values of `f`, but it does not throw any of them away: the function `f` can be recovered +from the distribution it defines. More generally, although a tempered distribution is not +*defined* by its values at points, it may still *have* well-defined values at points, and +those values are extractable when they exist. The distributional point of view does not +erase pointwise information where it is available; it simply refuses to demand it where +it is not. -For example, if the charge distribution is represented by the tempered distribution `ρ`, then -the charge registered by a device with weighting `φ` is `ρ φ`, or notionally `∫ ρ(x) φ(x) dx`. -For a point charge `q` at the origin this evaluates to `q · φ(0)`: the device "sees" the -charge weighted by the value of its response profile at the location of the charge, exactly as -physical intuition would suggest. +The electric field of a point charge illustrates both sides of this. The charge itself is +the Dirac delta `q δ(x - x₀)`, the tempered distribution sending each test function `φ` to +`q · φ(x₀)`: physically, the reading of a device with profile `φ` placed near the charge +is `q` weighted by the value of the profile at the location of the charge, exactly as +intuition suggests. The field it sources is the tempered distribution +`Eᵈ : φ ↦ ∫ E x · φ x dx`, where `E` is the Coulomb field +`E(x) = q (x - x₀) / (4π ε₀ |x - x₀|³)`. Away from `x₀` this field is smooth and has a +perfectly well-defined value at every point, and the distribution `Eᵈ` agrees with it +there; only at the location of the charge, where `E` diverges, is no pointwise value +available. The distributional formulation is precisely what allows the global object to be +defined in spite of this single bad point. -Derivatives still make sense in this framework, but they are defined by integration by parts. -If `f` is a tempered distribution, its derivative `∂f` is the distribution acting on test -functions by `(∂f) φ := - f (∂φ)`. For smooth `f` this reproduces the ordinary derivative -(the boundary terms vanish because Schwartz functions decay rapidly), but it also assigns a -meaningful derivative to objects such as the step function, whose distributional derivative -is the Dirac delta. This is what allows Maxwell's equations to retain their differential form -even when the sources are singular. +Derivatives also continue to make sense in this framework, but they are defined by +integration by parts. For a tempered distribution `f`, the derivative `∂f` is the +distribution acting on test functions by `(∂f) φ := - f (∂φ)`. When `f` is smooth this +reproduces the ordinary derivative — the boundary terms in the integration by parts vanish +because Schwartz functions decay rapidly — but it also assigns a meaningful derivative to +objects such as the step function, whose distributional derivative is the Dirac delta. +This is what allows Maxwell's equations to retain their differential form even when the +sources are singular. -Because pointwise values are no longer available, some constructions from classical -electromagnetism cease to be well defined in the distributional setting. The Lagrangian -density `ℒ = - Aᵤ Jᵘ - ¼ Fᵤᵥ Fᵘᵛ` is one such example: it relies on pointwise products of -distributions (such as `A` with `J`, or `F` with itself), and in general the product of two -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. +Not every classical construction survives the move to distributions, however. +This is because in general, one does not have access to the pointwise values of the distributions, +and many classical constructions rely on these. + he Lagrangian density `ℒ = - Aᵤ Jᵘ - ¼ Fᵤᵥ Fᵘᵛ` is a notable casualty: it relies on +pointwise products of distributions (`A` with `J`, and `F` with itself), and in general +the product of two 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 -surface `S`, classically `∫_S E · dA`, is no longer well defined, but one can still speak of -the flux weighted by a test function `φ`, notionally defined as `- ∫ E x · ∇ φ x dx`. -The intuition is that `φ` plays the role of a smoothed-out version of the region `V` -enclosed by `S`: imagine `φ` equal to `1` deep inside `V`, equal to `0` far outside, and -transitioning smoothly across `S` over a thin layer. Its gradient `∇ φ` is then nonzero only -in this transition layer, points inward (from `0` to `1`), and concentrates more sharply on -`S` the thinner the layer is made. By the divergence theorem, -`- ∫ E · ∇ φ dV = ∫ φ (∇ · E) dV`, which for a sharp `φ` is approximately the integral of -`∇ · E` over `V`, i.e. the flux of `E` out of `S`. As `φ` is taken to be a sharper and sharper -approximation of `V`, the weighted flux approaches the classical flux through `S`. The flux -through `S` itself is not directly accessible in the framework, since a perfectly sharp `φ` -(equal to `1` on `V` and `0` outside, with no smooth transition) is not a Schwartz map; but -it can be recovered as a limit of weighted fluxes over progressively sharper test functions. +Other classical constructions need only to be reformulated. Consider the flux of `E` out +of a surface `S`, classically `∫_S E · dA`. The natural distributional analogue is the +flux *weighted by a test function* `φ`, notionally `- ∫ E x · ∇ φ x dx`. Here `φ` plays +the role of a smoothed-out version of the region `V` enclosed by `S`. -In this setting, Gauss's law states precisely that the flux with weighting -`φ` equals the charge measured with the same weighting `φ` (with -an additional factor of `1/ε₀`). Notionally this is -`- ∫ E x · ∇ φ x dx = ∫ ρ x φ x dx / ε₀`. -In the distributional setting, this 'integral' form of Gauss's law -is exactly equivalent to the differential form `∇ · E = ρ / ε₀`, -due to the way derivatives are defined by integration by parts. +This does not mean the classical flux is lost. In the same way that a tempered +distribution may have well-defined values at points without being defined by them, it may +have a well-defined flux through a surface. Whenever +`E` is regular enough on `S` for `∫_S E · dA` to make sense — for instance when `S` +avoids any singularities of `E`, as for any sphere not centred on a point charge — the +weighted fluxes converge to this classical value as `φ` is sharpened, and the two notions +agree. The weighted formulation is what allows the flux to be discussed generally, +including in cases where the surface meets a singularity and the classical integral is +not directly available. + +In this setting Gauss's law takes a particularly clean form: the weighted flux equals the +charge measured with the same weighting, up to a factor of `1/ε₀`. Notionally, +`- ∫ E x · ∇ φ x dx = ∫ ρ x φ x dx / ε₀`. Because distributional derivatives are defined +by integration by parts, this 'integral' form is exactly equivalent to the differential +form `∇ · E = ρ / ε₀`, with no separate passage between the two. + +For points `x` where both `ρ` is defined, this distributional Gauss's law +implies that `∇ · E x = ρ x / ε₀`, as one would expect. -/