Physlib.Units.Integral

For a normed vector space $M$ over $\mathbb{R}$ equipped with a physical dimension (via the `HasDim` class) and a measurable structure where scalar multiplication is measurable, the type of measures $\mathcal{M}(M)$ is unit-dependent. The scaling of a measure $\mu \in \mathcal{M}(M)$ between two unit choices $u_1$ and $u_2$ is defined as the pushforward measure $f_* \mu$, where $f: M \to M$ is the map that scales elements of $M$ according to the change from $u_1$ to $u_2$.

Let $M$ be a measurable space equipped with a physical dimension. For any two systems of unit choices $u_1, u_2$ and any measure $\mu$ on $M$, the unit scaling of the measure $\mu$ is equal to the pushforward measure of $\mu$ under the scaling map of the underlying space. That is, $$\text{scaleUnit}(u_1, u_2, \mu) = f_* \mu$$ where $f: M \to M$ is the map defined by $f(m) = \text{scaleUnit}(u_1, u_2, m)$, which scales elements of $M$ according to the change from unit system $u_1$ to $u_2$.

Let $d$ be a physical dimension and $M$ be a measurable space. Let $[G]$ denote the physical dimension associated with the type $G$. The theorem states that the integral operator $$(\mu, f) \mapsto \int_M f(x) \, d\mu(x)$$ is dimensionally correct. Specifically, if $\mu$ is a measure on $M$ with dimension $d$, and $f: M \to G$ is a function with dimension $[G] \cdot d^{-1}$, then the resulting integral $\int f \, d\mu$ has the physical dimension $[G]$.