Commit 2025-10-03 10:42 4b5fe0e0

feat(Probability): Fernique's theorem for distributions that are invariant by rotation (#28343) Let μ be a finite measure on a second-countable normed space E such that the product measure μ.prod μ on E × E is invariant by rotation of angle -π/4. Then there exists a constant C > 0 such that the function x ↦ exp (C * ‖x‖ ^ 2) is integrable with respect to μ. The main application of this theorem will be for Gaussian measures.