Non-injective change of variables in integrals

Stream: maths

[Yury G. Kudryashov]

In #7693 I prove that $\int f(\|x\|)\,dx=n\operatorname{Vol}(B_1)\int_0^{\infty}f(r)r^{n-1}\,dr$, where $x\in E$, $n=\dim_{\mathbb R} E>0$, $f\colon \mathbb R\to F$, $\operatorname{Vol}(B_1)$ is the volume of a unit ball in $E$.
I wanted to have this formula for any f, not necessarily integrable, so the proof works in two steps: transfer the measure from $E\setminus \{0\}$ to $(0, \infty)\times\operatorname{sphere}(0, 1)$, then projection to the first coordinate.

[Yury G. Kudryashov]

It would be easier to prove that the push-forward of the Lebesgue measure on E under norm is the Lebesgue measure on real numbers with given density.

[Yury G. Kudryashov]

But this way the result will require f to be integrable.

[Yury G. Kudryashov]

@Sebastien Gouezel I know that you formalized a very advanced version of the change of variables formula. Is it true in case of a non-injective map (e.g., provided that we know that the push-forward in the Lebesgue measure with some density)?

[Yury G. Kudryashov]

If yes, how much different is the proof?

[Geoffrey Irving]

(deleted)

[Sebastien Gouezel]

If you already know the push-forward, then I guess the formula you want doesn't need anything more. docs#MeasureTheory.integral_map, for instance?

[Yury G. Kudryashov]

This lemma assumes that f is AEStronglyMeasurable.

[Yury G. Kudryashov]

We have a version without this assumption if φ is a measurable embedding. It is also true for Prod.fst, Prod.snd, and norm.

[Yury G. Kudryashov]

I wonder if there is a class of maps that generalizes Prod.fst/Prod.snd/norm. The only difficulty is to prove that AEStronglyMeasurable (f ∘ φ) implies AEStronglyMeasurable f under some assumptions on φ.

[Sebastien Gouezel]

Ah, sorry, I had missed the difficulty. Indeed, that's a good question!

[Anatole Dedecker]

"Has a measurable section" is the most natural thing that comes to mind and it seems to encompass your three use cases (assuming you mean nnnorm, but I don’t think the result could be true for norm)

[Yury G. Kudryashov]

How does a measurable section help?

[Yury G. Kudryashov]

Note that we need a statement about NullMeasurableSets, not MeasurableSets.

[Yury G. Kudryashov]

If we drop f, then the lemma we need is NullMeasurableSet (φ ⁻¹' s) μ <-> NullMeasurableSet s (μ.map φ).

[Yury G. Kudryashov]

(unless I miss something; I didn't formalize the implication)

[Felix Weilacher]

Is this different than what was being discussed in this thread?

[Felix Weilacher]

For example we showed there that if phi is a measurable map between standard Borel spaces with Borel image, then it is a quotient map for the null-measurable algebras

[Felix Weilacher]

And actually I think any measurable map will work.

[Yury G. Kudryashov]

Sorry, I forgot that I've already asked this question. I'll read the proof again tomorrow (have a test to grade ASAP).

[Xavier Roblot]

Yury G. Kudryashov said:

In #7693 I prove that $\int f(\|x\|)\,dx=n\operatorname{Vol}(B_1)\int_0^{\infty}f(r)r^{n-1}\,dr$, where $x\in E$, $n=\dim_{\mathbb R} E>0$, $f\colon \mathbb R\to F$, $\operatorname{Vol}(B_1)$ is the volume of a unit ball in $E$.
I wanted to have this formula for any f, not necessarily integrable, so the proof works in two steps: transfer the measure from $E\setminus \{0\}$ to $(0, \infty)\times\operatorname{sphere}(0, 1)$, then projection to the first coordinate.

Lately, I have been trying to prove a similar formula (which much less success than you :sweat_smile: ) since it provides a way to compute volume of unit balls in $\mathbb{R}^n$ (and also $\mathbb{C}^n$) for the norm $L_p$ (and also in mixed setting which is the one I really need). Is this something that you are planning to add?

[Yury G. Kudryashov]

Could you please give more details?

[Yury G. Kudryashov]

I mean, how do you want to compute the volume of the unit ball?

[Xavier Roblot]

To compute the volume of the unit ball for the norm $\|\cdot\|_p$, you take $f(x) = e ^ {-x ^p}$, so you get $\int f(\|x\|_p) dx = (\int_\mathbb{R} e ^ {- |x| ^ p} dx) ^ n$ where $n$ is the dimension. Then, you can compute all the integrals (that are equal to values of the Gamma function) and solve for $\mathrm{Vol}(B_1)$.

I think that works but I might be missing something.

[Yury G. Kudryashov]

Where does $\pi$ come from in this computation?

[Yury G. Kudryashov]

From some value of the Gamma function?

[Yury G. Kudryashov]

I guess, it comes from Gamma(1/2)

[Yury G. Kudryashov]

I meant, in the case p=2.

[Xavier Roblot]

Yes, the case p = 2 is done here: https://en.m.wikipedia.org/wiki/Volume_of_an_n-ball#Gaussian_integrals

[Xavier Roblot]

I guess I'll formalize these computations since I am the one that needs them.

[Xavier Roblot]

#8030