Moments of inertia tensor

Stream: PhysLean

[Joseph Tooby-Smith]

(This post is more to get this into the knowledge base of the project rather than anything else).

I was thinking about other places (in addition to electromagnetism and QM which are being discussed elsewhere) that distributions come up in physics, and one place is the moment of inertia tensor.

In the language of physics, given a 'mass distribution' $\rho(x)$ the moment of inertia tensor $I$ has components:

$$I_{ij} = \int d^3 x\; \rho(x) (x_k x_k \delta_{ij} - x_i x_j).$$

The interesting questions is what is the correct formalization of $\rho(x)$? The distributions currently defined in PhysLean are really 'tempered distributions', that is to say they are defined as continuous linear functions from Schwartz maps to some target. But, since $(x_k x_k \delta_{ij} - x_i x_j)$ is not a Schwartz map in $x$, I think here we require $\rho(x)$ to be restricted further to 'compactly supported distributions' which can equivalently be defined as continuous linear functions from smooth functions to some target.

From the point of view of physics this somewhat makes sense, it would be odd to give a moment of inertia to a distribution that was not 'compact'. But - alas, this requires making an API for compactly supported distributions in addition to tempered distributions.

(You really need some sort of distribution here due to 'point particles', 'thin rectangles', 'thin rods' etc)

[Joseph Tooby-Smith]

I hit a roadblock very early in trying to do anything along these lines, because I can't find the type corresponding to the vector space of smooth functions - if it even exists.

(One possible option is to use ContMDiffSection and the trivial vector bundle but this feels very obtuse)

[Tomas Skrivan]

Isn't the most natural space for $\rho$ to live in be the space of measures? Probably finite and compactly supported.

Why do you actually need the space of smooth functions? Shouldn't you just define the inertial tensor for $\rho$ be general function/distribution and then in all the theorems require it is compactly supported?

[Joseph Tooby-Smith]

Isn't the most natural space for ρ to live in be the space of measures? Probably finite and compactly supported.

I agree this is an option - and would probably work. Though I think distributions are (strictly) more general to work with then measures, in that every measure forms a distribution. Thus, I don't think there is any harm in using distributions, if it ends up working. But I would be happy to see it done this way.

Why do you actually need the space of smooth functions? Shouldn't you just define the inertial tensor for $ρ$ be general function/distribution and then in all the theorems require it is compactly supported?

Yes this is an option, one could just take distributions 𝓢(Space, ℝ) →L[ℝ] ℝ and enforce the condition that it is compactly supported where necessary. But every such distribution can be extending to a map C^⊤(Space, ℝ) →L[ℝ] ℝ , and it is really this map that we need to define the inertia tensor, because we need to know how it acts on $x_kx_k \delta_{ij} - x_ix_j$. So I thought it would be easier to just start with compact supported distributions defined directly through C^⊤(Space, ℝ) →L[ℝ] ℝ in the first place. Though maybe I am missing something here.

What I did manage to do in PhysLean#736 is define $\rho$ essentially as C^⊤(Space, ℝ) →ₗ[ℝ] ℝ , which isn't quite right as it needs to be continuous linear not just linear, but there is no definition of a topology on C^⊤(Space, ℝ) in Mathlib. I'm also not sure I know where the continuous part would be important in the story.