integral of a function of norm

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have a generic lemma about integrals like ∫ x : E, f ‖x‖ ∂μ (Bochner or Lebesgue)? Here μ is an additive Haar measure.

[Yury G. Kudryashov]

I want something like ∫ x : E, f ‖x‖ ∂μ = μ (ball (0 : E) 1) * n * ∫ r in Ioi 0, f r * r ^ (n - 1) (if I did computations correctly).

[Yury G. Kudryashov]

Probably, the right way to formulate this is to say that map norm μ = volume.withDensity _.

[Yury G. Kudryashov]

I'm going to add it.