Iterated integrals

Stream: Is there code for X?

[Xavier Roblot]

I would like to prove the following result:

example (n : ℕ) : volume {x : (Fin n) → ℝ | ∑ i, ‖x i‖ ≤ 1} =
    ENNReal.ofReal (2 ^ n / n.factorial)

the usual proof proceeds by induction using iterated integrals. However, I think that we are missing the necessary API. For example, I don't think we have the mesurableEquiv between (Fin (n+1) → ℝ) ≃ᵐ (Fin n → ℝ) × ℝ and the fact that it is MeasurePreserving? If there are missing, is there any plan to add them (preferably soon :sweat_smile: )?

On the other hand, maybe I am missing another simpler way to proceed.

[Kevin Buzzard]

At least for measure-preserving you should be able to use a Haar measure argument ("the product measure is translation-invariant and hence must be a constant multiple of the measure on R^{n+1} because we know this is Haar measure and there's only one up to constant")

[Xavier Roblot]

Kevin Buzzard said:

At least for measure-preserving you should be able to use a Haar measure argument ("the product measure is translation-invariant and hence must be a constant multiple of the measure on R^{n+1} because we know this is Haar measure and there's only one up to constant")

Yes, that's a good point.

[Sebastien Gouezel]

You have docs#MeasureTheory.measurePreserving_piFinSuccAboveEquiv

[Sebastien Gouezel]

@loogle MeasureTheory.MeasurePreserving, Fin _

[Xavier Roblot]

Sebastien Gouezel said:

You have docs#MeasureTheory.measurePreserving_piFinSuccAboveEquiv

Oh, that's great. I didn't know we had something like that. Thanks!

[Sebastien Gouezel]

@loogle MeasureTheory.MeasurePreserving, Fin _

[loogle]

:search: MeasureTheory.measurePreserving_finTwoArrow, MeasureTheory.measurePreserving_finTwoArrow_vec, and 8 more

[Sebastien Gouezel]

Maybe one in the list provided by loogle could even be more suited to your purposes. This tool is really awesome for this kind of question.

[Patrick Massot]

I've heard @Heather Macbeth and @Floris van Doorn have many tricks to work with iterated integrals.

[Kevin Buzzard]

Being able to work with them is also pretty awesome ;-)

[Heather Macbeth]

Yes, we haven't PR'd it yet but @Xavier Roblot it's in the same branch we were discussing on the #6907 thread.

[Antoine Chambert-Loir]

IIRC, @Sebastien Gouezel computed the volume an a Euclidean ball using the multiplicativity of the Gaussian integral. You could probably apply the same trick using $\exp(-|t|)$ inside of $\exp(-t^2)$.

[Xavier Roblot]

That does sound a lot more clever than what I am doing... Although, I'll probably need to think about it more to figure out how to make it work.