Commit 2025-10-09 08:14 dc9234a8

feat: Fernique's theorem for Gaussian distributions (#30167) For a Gaussian measure on a second-countable normed space, there exists C > 0 such that the function x ↦ exp (C * ‖x‖ ^ 2) is integrable. As a consequence, a Gaussian measure in a second-countable Banach space has finite moments of all orders.